Lemma gauss_clear_column_inv0 { m n : nat } (k_i : (⟦ m ⟧%stn)) (k_j : stn n) (iter : ⟦ S m ⟧%stn) (mat : Matrix F m n) (r : ⟦ m ⟧%stn) (r_gt_sep : r ≥ iter) : (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. } rewrite nat_rect_step. destruct (natgthorleh sep k_i). 2: { apply idpath. } rewrite gauss_clear_column_step_eq. unfold gauss_clear_column_step'. destruct (stn_eq_or_neq _ _). { unfold gauss_clear_column, gauss_clear_column_step. unfold gauss_clear_column in IH. now apply IH, natgthtogeh. } unfold gauss_clear_column in IH. rewrite add_row_mult_nontarget_row. 2: {now apply natlthtoneq. } rewrite IH. { apply idpath. } apply natgthtogeh, r_gt_sep. 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.