proposition: Lemma expfz_neq0 x n : x != 0 -> x ^ n != 0.
proof: Proof. by move=> x_nz; rewrite expfz_eq0; apply/nandP; right. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)