proposition: Lemma rowmxofK : cancel rowmxof vecof.
proof: Proof. move=> v; rewrite [v in RHS](coord_basis e_basis) ?memvf//. by apply: eq_bigr => i; rewrite !mxE. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)