proposition: Lemma hommx_mul (A : 'M_(m,n)) (B : 'M_(n, p)) : hommx e g (A *m B) = (hommx f g B \o hommx e f A)%VF.
proof: Proof. by apply: (can_inj (mxofK e_basis g_basis)); rewrite mxof_comp !hommxK. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)