proposition: Lemma vsof_sub M V : (vsof M <= V)%VS = (M <= msof V)%MS.
proof: Proof. apply/subvP/rV_subP => [MsubV _/submxP[u ->]|VsubM _/memv_imgP[u _ ->]]. by rewrite -mem_vecof MsubV// -rowmxof_sub vecofK// submxMl. by rewrite -[V]msofK -rowmxof_sub VsubM// -rowmxof_mul// submxMl. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)