proposition: Lemma msof0 : msof 0 = 0.
proof: Proof. apply/eqP; rewrite -submx0; apply/rV_subP => v. by rewrite -mem_vecof memv0 vecof_eq0// => /eqP->; rewrite sub0mx. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)