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