proposition: Lemma mulmx_addl : forall m n p (A1 A2 : 'M_(m, n)) (B : 'M_(n, p)), (A1 +m A2) *m B === A1 *m B +m A2 *m B.
proof: Proof. move=> m n p A1 A2 B i k; rewrite /addmx /mulmx. setoid_rewrite <- big_split. by 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