proposition: Lemma rpredZ_nat (S : addrClosed V) : {in nat_num & S, forall z u, z *: u \in S}.
proof: Proof. by move=> _ u /natrP[n ->]; apply: rpredZnat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)