proposition: Lemma addmx_block : forall m1 m2 n1 n2 (Aul Bul : 'M_(m1, n1)) (Aur Bur : 'M_(m1, n2)) (All Bll : 'M_(m2, n1)) (Alr Blr : 'M_(m2, n2)), block_mx Aul Aur All Alr +m block_mx Bul Bur Bll Blr === block_mx (Aul +m Bul) (Aur +m Bur) (All +m Bll) (Alr +m Blr).
proof: Proof. by move=> m1 m2 n1 n2 Aul Bul Aur Bur All Bll Alr Blr i j; rewrite/block_mx/pastemx/trmx/null_mx/addmx/oppmx/scalemx; case: split; case: split; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms