proposition: Lemma is_row_echelon_eq { m n : nat } (mat : Matrix F m n) : is_row_echelon mat -> ∏ i_1 i_2 : ⟦ m ⟧%stn, ∏ j_1 j_2 : ⟦ n ⟧%stn, i_1 < i_2 -> is_leading_entry (mat i_1) j_1 -> is_leading_entry (mat i_2) j_2 -> j_1 < j_2.
proof: Proof. destruct (natchoice0 n) as [contr_eq0 | p]. { unfold is_upper_triangular. intros ? ? ? j. apply fromstn0; now rewrite contr_eq0. } unfold is_row_echelon. intros H1 i_1 i_2 j_1 j_2 lt H2 H3. destruct (natgthorleh j_2 j_1) as [gt | leh]. { now apply gt. } destruct (H1 i_1 i_2) as [H4 H5]. destruct (natgthorleh j_2 j_1); try assumption. unfold is_leading_entry in H3. contradiction (pr1 H3). apply (H4 _ _ H2 lt leh). 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