proposition: Lemma submod_closedZ : submod_closed -> scaler_closed.
proof: Proof. by case=> S0 Slin a v Sv; rewrite -[a *: v]addr0 Slin. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)