proposition: Lemma mul1mx : forall m n (A : 'M_(m, n)), 1%:M *m A === A.
proof: Proof. by move=> m n A; rewrite -> mulmx_scalar, scale1mx; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms