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