proposition: 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: 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.
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