proposition: Lemma expgMn x y n : commute x y -> (x * y) ^+ n = x ^+ n * y ^+ n.
proof: Proof. move=> cxy; elim: n => [|n IHn]; first by rewrite mulg1. by rewrite !expgS IHn -mulgA (mulgA y) (commuteX _ (commute_sym cxy)) !mulgA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)