proposition: Lemma mulmx_paste : forall m n p1 p2 (A : 'M_(m, n)) (B1 : 'M_(n, p1)) (B2 : 'M_(n, p2)), A *m (pastemx B1 B2) === pastemx (A *m B1) (A *m B2).
proof: Proof. by move=> m n p1 p2 A B1 B2 i k; rewrite/pastemx/mulmx; case defk: (split k) => [k1 | k2]; apply eq_bigr=> j _; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms