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