proposition: Lemma vecofK : cancel vecof rowmxof.
proof: Proof. move=> v; apply/rowP=> i; rewrite !(lfunE, mxE). by rewrite coord_sum_free ?(basis_free e_basis). Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)