proposition: Lemma scalemxAr : forall m n p a (A : matrix R 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; apply trmx_inj. by rewrite -> trmx_scale, !trmx_mul, trmx_scale, scalemxAl; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms