proposition: Lemma rpredZint (R : ringType) (M : lmodType R) (S : zmodClosed M) m : {in S, forall u, m%:~R *: u \in S}.
proof: Proof. by move=> u Su; rewrite /= scaler_int rpredMz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)