proposition: Lemma exprz_out x n (nux : x \isn't a GRing.unit) (hn : 0 <= n) : x ^ (- n) = x ^ n.
proof: Proof. by case: (intP n) hn=> //= m; rewrite -exprnN -exprVn invr_out. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)