proposition: Lemma is_row_echelon_nil_matrix {m n : nat} {A : Matrix F m n} (eq0 : n = 0) : (@is_row_echelon _ m n A).
proof: Proof. unfold is_row_echelon; intros i_1 i_2. use tpair. { intros ?; apply fromstn0; now rewrite <- eq0. } simpl; intros eq ?. rewrite <- eq. apply funextfun; intros j. apply fromstn0; rewrite <- eq0; exact j. Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSequences UniMath.Combinatorics.Vectors UniMath.Combinatorics.Maybe UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.RowOps