proposition: Lemma mulmxA : forall m n p q (A : 'M_(m, n)) (B : 'M_(n, p)) (C : 'M_(p, q)), A *m (B *m C) === A *m B *m C.
proof: Proof. move=> m n p q A B C i l; rewrite/mulmx. setoid_rewrite big_distrr; setoid_rewrite big_distrl. setoid_rewrite (exchange_big predT predT (fun j k => A i j * (B j k * C k l))). by apply eq_bigr=> j _; apply eq_bigr=> k _; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms