Lemma gauss_clear_column_as_left_matrix_inv0 { m n : nat } (iter : stn (S m)) (mat : Matrix F m n) (k_i : (⟦ m ⟧%stn)) (k_j : (stn n)) (i : ⟦ m ⟧%stn) (i_leh_k : i ≤ k_i) : (gauss_clear_column_as_left_matrix iter mat k_i k_j ** mat) i = mat i. Proof. unfold gauss_clear_column_as_left_matrix. destruct iter as [iter p]. induction iter as [| iter IH]; intros. { simpl; now rewrite matlunax2. } unfold gauss_clear_column_as_left_matrix. rewrite nat_rect_step. destruct (natgthorleh iter k_i) as [gt | _]. 2: {rewrite matlunax2; now rewrite IH. } assert (lt: iter < S m). {apply (istransnatlth _ _ _ (natgthsnn iter) p). } rewrite <- (IH lt). rewrite IH, matrix_mult_assoc, add_row_mult_as_matrix. 2: {now apply issymm_natneq, natgthtoneq. } rewrite add_row_mult_nontarget_row. 2: {apply natgthtoneq. apply (natlehlthtrans _ _ _ i_leh_k gt). } now rewrite IH. 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.