proposition: Lemma commrXz_wmulls x y n : 0 <= n -> GRing.comm x y -> (x * y) ^ n = x ^ n * y ^ n.
proof: Proof. move=> n0 com_xy; elim: n n0 => [|n _|n _] //; first by rewrite expr0z mulr1. by rewrite -!exprnP exprMn_comm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)