proposition: Lemma mx_row'_eq : forall m n i0 (A B : 'M_(m, n)), mx_row' i0 A === mx_row' i0 B -> {in predC1 i0, forall i, A i === B i}.
proof: Proof. move=> m n i0 A B eqAB i; rewrite /mx_row' inE /= eq_sym. by case/unlift_some=> i' -> _; apply: eqAB. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms