proposition: Lemma scalemxAl : forall m n p a (A : 'M_(m, n)) (B : 'M_(n, p)), a *m: (A *m B) === (a *m: A) *m B.
proof: Proof. move=> m n p a A B i k. rewrite/scalemx/mulmx. setoid_rewrite (big_distrr). 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