proposition: Lemma scalemx_block : forall m1 m2 n1 n2 a (Aul : 'M_(m1, n1)) (Aur : 'M_(m1, n2)) (All : 'M_(m2, n1)) (Alr : 'M_(m2, n2)), a *m: block_mx Aul Aur All Alr === block_mx (a *m: Aul) (a *m: Aur) (a *m: All) (a *m: Alr).
proof: Proof. by move=> m1 m2 n1 n2 a Aul Aur All Alr 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