proposition: Lemma mx_row_id : forall n (A : 'M_(1, n)), mx_row ord0 A === A.
proof: Proof. by move=> n A i j; (have -> : ord0 = i by rewrite (ord1 i); apply ord_inj => //); reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms