proposition: Lemma rpredZ_int (S : zmodClosed V) : {in int_num & S, forall z u, z *: u \in S}.
proof: Proof. by move=> _ u /intrP[m ->] ?; rewrite scaler_int rpredMz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)