proposition: Lemma hommxK : cancel hommx mxof.
proof: Proof. move=> M; apply/matrixP => i j; rewrite !mxE/= lfunE/=. by rewrite /funmx vecofK// -rowE coord_vecof// mxE. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)