proposition: Lemma rpredZeq (S : submodClosed V) a v : (a *: v \in S) = (a == 0) || (v \in S).
proof: Proof. have [-> | nz_a] := eqVneq; first by rewrite scale0r rpred0. by apply/idP/idP; first rewrite -{2}(scalerK nz_a v); apply: rpredZ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)