proposition: Lemma tprodE m1 n1 p1 (A1 :'M[F]_(m1,n1)) (A2 :'M[F]_(n1,p1)) m2 n2 p2 (B1 :'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) : tprod (A1 *m A2) (B1 *m B2) = (tprod A1 B1) *m (tprod A2 B2).
proof: Proof. elim: m1 n1 p1 A1 A2 m2 n2 p2 B1 B2 => /= [|m1 IH]. by move=> *; rewrite mul0mx. move=> n1 p1 A1 A2 m2 n2 p2 B1 B2. rewrite mul_col_mx -IH. congr col_mx; last by rewrite dsumx_mul. rewrite usumx_mul. elim: n1 {A1}(usubmx (A1: 'M_(1 + m1, n1))) p1 A2=> //= [u p1 A2|]. by rewrite [A2](flatmx0) !mulmx0 -trowbE linear0. move=> n1 IH1 A p1 A2 //=. set Al := lsubmx _; set Ar := rsubmx _. set Su := usubmx _; set Sd := dsubmx _. rewrite mul_row_col -IH1. rewrite -{1}(@hsubmxK F 1 1 n1 A). rewrite -{1}(@vsubmxK F 1 n1 p1 A2). rewrite (@mul_row_col F 1 1 n1 p1). rewrite -trowbE linearD /= trowbE -/Al. congr (_ + _). rewrite {1}[Al]mx11_scalar mul_scalar_mx. by rewrite -trowbE linearZ /= trowbE -/Su trow_mul scalemxAl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)