proposition: Lemma commuteX2 x y m n : commute x y -> commute (x ^+ m) (y ^+ n).
proof: Proof. by move=> cxy; apply/commuteX/commute_sym/commuteX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)