proposition: Lemma scalemx_subr : forall x A B, x *m: (A -m B) === (x *m: A) -m (x *m: B).
proof: Proof. by rewrite/null_mx/addmx/oppmx/scalemx=> x A B i j; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms