Lemma gauss_clear_column_inv3 { m n : nat } (k_i : (⟦ m ⟧%stn)) (k_j : (⟦ n ⟧%stn)) (iter : ⟦ S m ⟧%stn) (mat : Matrix F m n) (p' : mat k_i k_j != 0%ring) : ∏ r : (⟦ m ⟧%stn), r < iter -> r > k_i -> ((gauss_clear_column mat k_i k_j iter) r k_j = 0%ring). Proof. destruct iter as [sep p]. intros r r_le_sep r_gt_k. rewrite (gauss_clear_column_inv2 k_i k_j (sep ,, p) mat r r_le_sep) , <- gauss_clear_column_step_eq. 2: {exact r_gt_k. } rewrite (gauss_clear_column_step_inv1 k_i k_j r mat); try easy. now apply natgthtoneq. 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.