proposition: Lemma rpredXsign (R : unitRingType) (S : divClosed R) n x : (x ^ ((-1) ^+ n) \in S) = (x \in S).
proof: Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)