Lemma gauss_clear_rows_up_to_inv1 { m n : nat } (mat : Matrix F m n) (p : n > 0) (row_sep : (⟦ S m ⟧%stn)) : is_row_echelon_partial_1 (gauss_clear_rows_up_to mat row_sep) row_sep. Proof. unfold gauss_clear_rows_up_to. destruct row_sep as [row_sep p'']. induction row_sep as [| row_sep IH]. { simpl; intros ? ? ? ? contr; contradiction (negnatlthn0 n contr). } rewrite nat_rect_step. set (inner := nat_rect _ _ _ _). set (lt' := (istransnatlth _ _ _ (natgthsnn row_sep) p'')). apply (gauss_clear_row_inv0 (inner lt') p (row_sep,, lt') _), IH. 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.