proposition: Lemma exprz_exp x m n : (x ^ m) ^ n = (x ^ (m * n)).
proof: Proof. wlog: n / 0 <= n. by case: n=> [n -> //|n]; rewrite ?NegzE mulrN -?invr_expz=> -> /=. elim: n x m=> [|n ihn|n ihn] x m // _; first by rewrite mulr0 !expr0z. rewrite exprSz ihn // intS mulrDr mulr1 exprzD_ss //. by case: (intP m)=> // m'; rewrite ?oppr_le0 //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)