Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996) Theorems shortened and reordered. (Revised by Wolf Lammen, 9-Apr-2022)