Lemma gauss_clear_rows_up_to_inv0 { m n : nat } (mat : Matrix F m n) (row_sep : (⟦ S m ⟧%stn)) (p : n > 0) : ∏ i_1 : ⟦ m ⟧%stn, i_1 < row_sep -> (gauss_clear_rows_up_to mat row_sep) i_1 = const_vec 0%ring -> ∏ i_2 : ⟦ m ⟧%stn, i_1 < i_2 -> (gauss_clear_rows_up_to mat row_sep) i_2 = const_vec 0%ring. Proof. unfold is_row_echelon_partial_2. intros i_1 i1_lt_rowsep no_leading. unfold gauss_clear_rows_up_to in *. destruct row_sep as [row_sep lt]. induction row_sep as [| row_sep IH]. {contradiction (negnatgth0n i_1 i1_lt_rowsep). } rename i1_lt_rowsep into i1_lt_srowsep. set (lt' := (istransnatlth _ _ _ (natgthsnn row_sep) lt)). rewrite nat_rect_step in no_leading |- *. unfold gauss_clear_row in IH, no_leading |- *. destruct (natchoice0 n) as [contr_eq | gt]. { rewrite contr_eq in p. contradiction (isirreflnatgth _ p). } revert no_leading. destruct (natlehchoice i_1 row_sep) as [i1_lt_rowsep | eq]. {apply natlthsntoleh. assumption. } - destruct (select_uncleared_column _ _) as [[piv_c [_ [piv_r [leh [neq0 eq0]]]]] | none]; simpl. 2: { now apply IH. } intros ? ? i1_lt_i2. destruct (natgthorleh i_2 row_sep) as [i2_gt_rowsep | i2_le_rowsep]. + rewrite switch_row_equal_rows in no_leading; try assumption. * rewrite gauss_clear_column_inv1 in no_leading. 2: { now apply natlthtoleh. } rewrite gauss_clear_column_inv2; try assumption. 2: {apply (pr2 i_2). } unfold gauss_clear_column_step'. destruct (stn_eq_or_neq _ _) as [contr_eq | ?]. { contradiction (isirreflnatgth row_sep). now rewrite contr_eq in * |-. } rewrite add_row_mult_source_row_zero; try assumption. -- rewrite switch_row_equal_rows. ++ now rewrite IH. ++ do 2 (rewrite IH; try easy). apply (natgehgthtrans _ _ _ leh i1_lt_rowsep). -- rewrite switch_row_equal_rows; try assumption. ++ now rewrite IH. ++ do 2 (rewrite IH; try assumption; try reflexivity). apply (natgehgthtrans _ _ _ leh i1_lt_rowsep). * rewrite gauss_clear_column_inv1 in no_leading. 2: { now apply natlthtoleh. } rewrite switch_row_other_row' in no_leading. 3: { apply natlthtoneq, (natgehgthtrans _ _ _ leh i1_lt_rowsep). } 2: { now apply natlthtoneq. } do 2 (rewrite IH; try easy). apply (natgehgthtrans _ _ _ leh i1_lt_rowsep). + rewrite switch_row_equal_rows in no_leading; try assumption. * rewrite gauss_clear_column_inv1 in no_leading. 2: { apply natgthtogeh in i1_lt_i2; apply (istransnatleh i1_lt_i2 i2_le_rowsep). } rewrite gauss_clear_column_inv1; try assumption. rewrite switch_row_equal_rows; try assumption. -- now rewrite IH. -- do 2 (rewrite IH; try easy). apply (natgehgthtrans _ _ _ leh i1_lt_rowsep). * rewrite gauss_clear_column_inv1 in no_leading. 2: { now apply natlthtoleh in i1_lt_rowsep. } rewrite switch_row_other_row' in no_leading. 3: { apply natlthtoneq, (natgehgthtrans _ _ _ leh i1_lt_rowsep). } 2: { apply natlthtoneq, (natlthlehtrans _ _ _ i1_lt_i2 i2_le_rowsep). } do 2 (rewrite IH; try easy). apply (natgehgthtrans _ _ _ leh i1_lt_rowsep). - intros; unfold gauss_clear_row in * |-. destruct (select_uncleared_column _ _) as [[? [? [? [? [neq0 ?]]]]] | no_col]. 2: { apply funextfun; intros j_2. assert (le : row_sep ≤ i_2). {apply natgthtogeh. now rewrite <- eq. } apply no_col; try assumption. apply (pr2 j_2). } unfold leading_entry_compute in no_leading. contradiction neq0. refine (const_vec_eq _ _ _ _). rewrite <- no_leading. unfold switch_row. rewrite gauss_clear_column_inv1. 2: { rewrite eq. apply isreflnatleh. } destruct (stn_eq_or_neq _ _); destruct (stn_eq_or_neq _ _) as [? | contr_neq]; try reflexivity; contradiction (nat_neq_to_nopath contr_neq). 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.