proposition: Lemma scalar_mx_opp : forall (n : nat) a, (- a)%:M === -m (@scalar_mx n a).
proof: Proof. by move=> n a i j; rewrite/block_mx/pastemx/trmx/null_mx/addmx/oppmx/scalemx/scalar_mx/mulmx; case: eqP=> _; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms