Lemma gauss_clear_column_inv4 { m n : nat } (mat : Matrix F m n) (k_i : (⟦ m ⟧%stn)) (k_j : stn n) (iter : ⟦ S m ⟧%stn) (j : ⟦ n ⟧%stn) (eq0 : mat k_i j = 0%ring) : ∏ i : ⟦ m ⟧%stn, gauss_clear_column mat k_i k_j iter i j = mat i j. Proof. unfold gauss_clear_column. destruct iter as [iter lt]. induction iter as [| iter IH]. { easy. } intros i. rewrite nat_rect_step, gauss_clear_column_step_eq. destruct (stn_eq_or_neq (iter,, lt) k_i) as [eq | ?]. - rewrite <- eq. destruct (natgthorleh _ _) as [contr | ?]. { now apply isirreflnatgth in contr. } reflexivity. - rewrite <- (IH (istransnatlth _ _ _ (natlthnsn iter) lt)) , <- gauss_clear_column_step_eq. unfold gauss_clear_column_step'. destruct (natgthorleh _ _) as [_ | _]. 2: { now rewrite IH. } rewrite gauss_clear_column_step_eq. unfold gauss_clear_column_step'. destruct (stn_eq_or_neq _ _); try reflexivity. unfold add_row_mult. destruct (stn_eq_or_neq _ _) as [eq | ?]; try apply coprod_rect_compute_1; try apply coprod_rect_compute_2. + rewrite coprod_rect_compute_1. do 3 rewrite IH. now rewrite eq0, <- eq, (@rigmultx0 F), (@rigrunax1 F). + now rewrite coprod_rect_compute_2. 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.