proposition: Lemma mx_row0 : forall m n i0, mx_row i0 (@null_mx m n) === (@null_mx 1 n).
proof: Proof. by move=> m n; rewrite/trmx/null_mx/addmx/oppmx/scalemx; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms