proposition: Lemma unitr_n0expz x n : n != 0 -> (x ^ n \is a GRing.unit) = (x \is a GRing.unit).
proof: Proof. by case: n => *; rewrite ?NegzE -?exprz_inv ?unitrX_pos ?unitrV ?lt0n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)