proposition: Lemma scalemx_addl : forall x y A, (x + y) *m: A === (x *m: A) +m (y *m: A).
proof: Proof. by rewrite/null_mx/addmx/oppmx/scalemx=> x y A 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