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. 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices. Require Import UniMath.Algebra.GaussianElimination.RowOps.