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