proposition: Lemma mulmx_block : forall m1 m2 n1 n2 p1 p2 (Aul : matrix R m1 n1) Aur All Alr Bul Bur Bll Blr, (block_mx Aul Aur All Alr : 'M_(m1 + m2, n1 + n2)) *m (block_mx Bul Bur Bll Blr : 'M_(n1 + n2, p1 + p2)) === block_mx (Aul *m Bul +m Aur *m Bll) (Aul *m Bur +m Aur *m Blr) (All *m Bul +m Alr *m Bll) (All *m Bur +m Alr *m Blr).
proof: Proof. move=> m1 m2 n1 n2 p1 p2 Aul Aur All Alr Bul Bur Bll Blr/=; rewrite <- (trmxK (_ *m _)). rewrite -> trmx_mul_rev, (trmx_block Aul); rewrite /block_mx; rewrite -> (trmxK (pastemx _ _)), dotmx_paste, <- !addmx_paste. by rewrite -> !trmx_add, (trmxK _), (trmxK _), <- addmx_paste, !mulmx_paste, <- !trmx_mul_rev, !mulmx_paste; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms