proposition: Lemma pastemx0 : forall m n1 n2, pastemx (@null_mx m n1) (@null_mx m n2) === (@null_mx m (n1 + n2)).
proof: Proof. by move=> m n1 n2 i j; rewrite/pastemx/trmx/null_mx/addmx/oppmx/scalemx; case: split; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms