Lemma gauss_clear_column_step_inv1 {m n : nat} (r_pivot : ⟦m⟧%stn) (c_pivot : ⟦ n ⟧%stn) (r : (⟦ m ⟧%stn)) (mat : Matrix F m n) (p_1 : mat r_pivot c_pivot != 0%ring) (p_2 : r ≠ r_pivot) : (gauss_clear_column_step r_pivot c_pivot r mat) r c_pivot = 0%ring. Proof. intros; unfold gauss_clear_column_step. destruct (stn_eq_or_neq r r_pivot) as [p | _]. { rewrite p in p_2. now apply isirrefl_natneq in p_2. } rewrite add_row_mult_as_matrix. 2: { now apply issymm_natneq. } rewrite add_row_mult_target_row. rewrite <- (@ringlmultminus F), ringassoc2. etrans. { now apply maponpaths, maponpaths, fldmultinvlax'. } rewrite (@rigrunax2 F); apply ringrinvax1. 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.