proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSequences UniMath.Combinatorics.Vectors UniMath.Combinatorics.Maybe UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.RowOps