proposition: Lemma vsof_eq0 M : (vsof M == 0%VS) = (M == 0).
proof: Proof. rewrite (sameP eqP eqmx0P) -!(eqmxP (vsofK M)) (sameP eqmx0P eqP) -msof0. by rewrite (inj_eq (can_inj msofK)). Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)