proposition: Lemma exprMn_comm x y n : comm x y -> (x * y) ^+ n = x ^+ n * y ^+ n.
proof: Proof. move=> com_xy; elim: n => /= [|n IHn]; first by rewrite mulr1. by rewrite !exprS IHn !mulrA; congr (_ * _); rewrite -!mulrA -commrX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)