proposition: Lemma rpredXz (R : unitRingType) (S : divClosed R) m : {in S, forall x, x ^ m \in S}.
proof: Proof. by case: m => n x Sx; rewrite ?rpredV rpredX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)