proposition: Lemma rpredMz (M : zmodType) (S : zmodClosed M) m : {in S, forall u, u *~ m \in S}.
proof: Proof. by case: m => n u Su; rewrite ?rpredN ?rpredMn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)