proposition: Lemma exprMz_comm x y n : x \is a GRing.unit -> y \is a GRing.unit -> GRing.comm x y -> (x * y) ^ n = x ^ n * y ^ n.
proof: Proof. move=> ux uy com_xy; elim: n => [|n _|n _]; first by rewrite expr0z mulr1. by rewrite -!exprnP exprMn_comm. rewrite -!exprnN -!exprVn com_xy -exprMn_comm ?invrM//. exact/commrV/commr_sym/commrV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)