proposition: Lemma unitrXz x n (ux : x \is a GRing.unit) : x ^ n \is a GRing.unit.
proof: Proof. case: (intP n)=> {n} [|n|n]; rewrite ?expr0z ?unitr1 ?unitrX //. by rewrite -invr_expz unitrV unitrX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)