Lemma gauss_clear_column_step_inv3 {m n : nat} (k_i : stn m) (k_j : (⟦ n ⟧%stn)) (r : (⟦ m ⟧%stn)) (mat : Matrix F m n) (j : ⟦ m ⟧%stn) (j' : stn n) (p : r < j) : (gauss_clear_column_step k_i k_j j mat) r j' = mat r j'. Proof. assert (p': r ≠ j). {now apply issymm_natneq, natgthtoneq. } now rewrite (gauss_clear_column_step_inv2 k_i k_j r mat j p'). 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.