proposition: Lemma exprzDr x (ux : x \is a GRing.unit) m n : x ^ (m + n) = x ^ m * x ^ n.
proof: Proof. move: n m; apply: wlog_le=> n m hnm. by rewrite addrC hnm commrXz //; exact/commr_sym/commrXz. case: (intP m) hnm=> {m} [|m|m]; rewrite ?mul1r ?add0r //; case: (intP n)=> {n} [|n|n _]; rewrite ?mulr1 ?addr0 //; do ?by rewrite exprzD_ss. rewrite -invr_expz subzSS !exprSzr invrM ?unitrX // -mulrA mulVKr //. case: (leqP n m)=> [|/ltnW] hmn; rewrite -{2}(subnK hmn) exprzD_nat -subzn //. by rewrite mulrK ?unitrX. by rewrite invrM ?unitrXz // mulVKr ?unitrXz // -opprB -invr_expz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)