proposition: Lemma exprzD_ss x m n : (0 <= m) && (0 <= n) || (m <= 0) && (n <= 0) -> x ^ (m + n) = x ^ m * x ^ n.
proof: Proof. case: (intP m)=> {m} [|m|m]; case: (intP n)=> {n} [|n|n] //= _; by rewrite ?expr0z ?mul1r ?exprzD_nat ?exprzD_Nnat ?sub0r ?addr0 ?mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)