proposition: Lemma commrXz x y n : GRing.comm x y -> GRing.comm x (y ^ n).
proof: Proof. rewrite /GRing.comm; elim: n x y=> [|n ihn|n ihn] x y com_xy //=. * by rewrite expr0z mul1r mulr1. * by rewrite -exprnP commrX //. rewrite -exprz_inv -exprnP commrX //. case: (boolP (y \is a GRing.unit))=> uy; last by rewrite invr_out. by apply/eqP; rewrite (can2_eq (mulrVK _) (mulrK _)) // -mulrA com_xy mulKr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)