Lemma gauss_clear_column_inv1 { m n : nat } (k_i : (⟦ m ⟧%stn)) (k_j : stn n) (r : stn m) (iter : ⟦ S m ⟧%stn) (p' : r ≤ k_i) (mat : Matrix F m n) : (gauss_clear_column mat k_i k_j iter) r = mat r. Proof. unfold gauss_clear_column. destruct iter as [sep p]. induction sep as [| sep IH]. {easy. } unfold gauss_clear_column. apply funextfun. intros q. rewrite nat_rect_step. destruct (natgthorleh _ _)as [gt | ?]; try reflexivity. rewrite gauss_clear_column_step_inv3. 2 : {now refine (natgthgehtrans _ _ _ gt _). } unfold gauss_clear_column in IH. now rewrite 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.