proposition: Lemma dotmx_paste : forall m n1 n2 p A1 A2 B1 B2, (pastemx A1 A2 : 'M_(m, n1 + n2)) *m (pastemx B1 B2 : 'M_(p, n1 + n2))^T === A1 *m B1^T +m A2 *m B2^T.
proof: Proof. move=> m n1 n2 p A1 A2 B1 B2 i k; rewrite/mulmx/addmx/trmx; setoid_rewrite big_split_ord. by apply radd_morph; apply eq_bigr=> j _; [rewrite -> pastemxEl, pastemxEl | rewrite -> pastemxEr, pastemxEr]; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms