proposition: Lemma mulmx_addr : forall m n p (A : 'M_(m, n)) (B1 B2 : 'M_(n, p)), A *m (B1 +m B2) === A *m B1 +m A *m B2.
proof: Proof. by move=> m n p A B1 B2 i k; rewrite/mulmx/addmx; setoid_rewrite <- big_split; apply eq_bigr=> j _; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms