proposition: Lemma gauss_clear_column_step_inv2 {m n : nat} (k_i : stn m) (k_j : (⟦ n ⟧%stn)) (r : (⟦ m ⟧%stn)) (mat : Matrix F m n) (j : ⟦ m ⟧%stn) (p : r ≠ j) : (gauss_clear_column_step k_i k_j j mat) r = mat r.
proof: Proof. intros. rewrite gauss_clear_column_step_eq. unfold gauss_clear_column_step'. destruct (stn_eq_or_neq j k_i). { apply idpath. } apply funextfun; intros ?. rewrite add_row_mult_nontarget_row; try reflexivity. now apply issymm_natneq. 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