proposition: 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: 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.
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