proposition: Lemma expfz_n0addr x m n : m + n != 0 -> x ^ (m + n) = x ^ m * x ^ n.
proof: Proof. have [-> hmn|nx0 _] := eqVneq x 0; last exact: expfzDr. rewrite !exp0rz (negPf hmn). case: (eqVneq m 0) hmn => [->|]; rewrite (mul0r, mul1r) //. by rewrite add0r=> /negPf->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)