proposition: Lemma matrix_comp k l m n (E : 'I_k -> 'I_l -> T) (F : 'I_n -> 'I_k) G : \matrix_(i < n, j < m) ((\matrix_(i0 < k, j0 < l) E i0 j0) (F i) (G j)) = \matrix_(i, j) (E (F i) (G j)).
proof: Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
imports: mathcomp(all_ssreflect all_algebra)