proposition: Lemma msof_sub V M : (msof V <= M)%MS = (V <= vsof M)%VS.
proof: Proof. apply/rV_subP/subvP => [VsubM v vV|MsubV _/submxP[u ->]]. by rewrite -rowmxof_sub VsubM// -mem_vecof rowmxofK. by rewrite mul_mxof rowmxof_sub MsubV// memv_proj. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)