Lemma clear_column_eq_matrix_def { m n : nat } (iter : ⟦ S m ⟧%stn) (k_i : (⟦ m ⟧%stn)) (k_j : (⟦ n ⟧%stn)) (mat : Matrix F m n) : ((gauss_clear_column_as_left_matrix iter mat k_i k_j) ** mat) = gauss_clear_column mat k_i k_j iter. Proof. intros. destruct iter as [iter p]. set (p' := (stn_implies_ngt0 k_i)). induction iter as [| iter IH]; try apply matlunax2. unfold gauss_clear_column, gauss_clear_column_as_left_matrix. unfold gauss_clear_column, gauss_clear_column_as_left_matrix in IH. do 2 rewrite nat_rect_step. rewrite gauss_clear_column_step_eq. destruct (natgthorleh iter k_i) as [gt | leh]. 2 : { rewrite matlunax2; rewrite IH. induction iter as [| iter IH']; try apply idpath. rewrite nat_rect_step. destruct (natgthorleh iter k_i) as [gt' | ?]; try apply idpath. apply natgehsntogth in gt'. apply fromempty, (isasymmnatgth _ _ gt' leh). } rewrite matrix_mult_assoc, <- IH. unfold gauss_clear_column_step'. destruct (stn_eq_or_neq _ _) as [eq | neq]. { apply fromempty. apply neggth_logeq_leh in gt; try assumption. rewrite <- eq. apply isreflnatgeh. } rewrite add_row_mult_as_matrix. 2 : { now apply issymm_natneq, natgthtoneq. } apply pathsinv0, maponpaths_2. etrans. { set (f := @gauss_clear_column_as_left_matrix_inv0 m n). unfold gauss_clear_column_as_left_matrix in f. set (lt' := (istransnatlth _ _ _ (natgthsnn iter) p)). change iter with (pr1 (make_stn _ iter lt')). change (istransnatlth _ _ _ _ p) with (make_stn _ iter lt'). rewrite (f (make_stn _ iter lt') _ _ _ _ (isreflnatleh k_i)). change (pr1 (make_stn _ iter lt')) with iter. change (make_stn _ iter lt') with (istransnatlth _ _ _ _ p) . reflexivity. } apply maponpaths_1, maponpaths_2. rewrite IH. pose (H := @gauss_clear_column_inv0). unfold gauss_clear_column in H. set (lt' := (istransnatlth _ _ _ (natgthsnn iter) p)). change iter with (pr1 (make_stn _ iter lt')). change (istransnatlth _ _ _ _ p) with (make_stn _ iter lt'). rewrite H; try easy. apply isreflnatleh. 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.