proposition: Lemma gauss_clear_row_inv0 { m n : nat } (mat : Matrix F m n) (p : n > 0) (row_sep : (⟦ S m ⟧%stn)) (p' : row_sep < m) : is_row_echelon_partial_1 mat row_sep -> is_row_echelon_partial_1 (gauss_clear_row mat (pr1 row_sep,, p')) (S (pr1 row_sep),, p').
proof: Proof. intros H1. unfold is_row_echelon_partial_1. unfold gauss_clear_rows_up_to. intros i_1 i_2 j_1 j_2 i1_lt H2 i1_lt_i2 j1_lt_j2. revert H2; unfold gauss_clear_row; clear p. destruct (natchoice0 n) as [contr_eq | p]. { apply fromstn0. now rewrite contr_eq. } destruct (select_uncleared_column _ _) as [[piv_c [_ [piv_r [leh [neq0 eq0]]]]] | none]; simpl. 2 : { intros isle. destruct (natlehchoice i_1 (pr1 row_sep)) as [? | eq]; try assumption. { rewrite (H1 i_1 i_2 j_1 j_2); try easy. } rewrite none; intros; try easy. 2: { exact (pr2 (j_1)). } apply natgthtogeh; simpl. now rewrite <- eq. } intros is_le. rewrite gauss_clear_column_inv1 in is_le. 2 : { now apply natlthsntoleh. } destruct (natlehchoice i_1 (pr1 row_sep)) as [lt | eq]. { now apply natlthsntoleh. } { rewrite switch_row_other_row' in is_le. 3: { apply natlthtoneq. refine (natlthlehtrans _ _ _ lt leh). } 2: { now apply natlthtoneq. } rewrite gauss_clear_column_inv4. { rewrite switch_row_equal_entries. - now rewrite (H1 i_1 i_2 j_1 j_2). - do 2 (rewrite (H1 i_1 _ j_1 j_2); try easy). refine (natlthlehtrans _ _ _ lt leh). } rewrite switch_row_equal_entries. + rewrite (H1 i_1 _ j_1 j_2); easy. + do 2 (rewrite (H1 i_1 _ j_1 j_2); try easy). refine (natlthlehtrans _ _ _ lt leh). } destruct (natgthorleh piv_c j_1). { rewrite gauss_clear_column_inv4; try easy. - unfold switch_row. destruct (stn_eq_or_neq _ _) as [eq' | neq]; simpl. + destruct (stn_eq_or_neq _ _) as [contr_eq | neq']; simpl. { now rewrite eq0. } rewrite eq0; try easy. apply (isreflnatleh). + destruct (stn_eq_or_neq _ _) as [contr_eq | neq']; simpl. { now rewrite eq0. } rewrite eq0; try easy. rewrite <- (stn_eq_2 _ _ eq). now apply natgthtogeh. - rewrite switch_row_equal_entries; (rewrite eq0; try easy; try apply isreflnatleh). now rewrite eq0. } destruct (natlehchoice piv_c j_1) as [gt | eq']; try assumption. 2 : { rewrite (stn_eq j_1 piv_c (!eq')). rewrite gauss_clear_column_inv3; try easy. - unfold switch_row. rewrite stn_eq_or_neq_refl; simpl. apply neq0. - exact (pr2 i_2). - now rewrite <- (stn_eq_2 _ _ eq). } contradiction neq0. destruct (natlehchoice i_1 (pr1 row_sep)) as [lt | eq']. { now apply natlthsntoleh. } - rewrite switch_row_other_row' in is_le. 3: { apply natlthtoneq. refine (natlthlehtrans _ _ _ lt leh). } 2: { now apply natlthtoneq. } refine (H1 _ _ _ _ lt is_le _ _). + refine (natlthlehtrans _ _ _ lt leh). + now refine (istransnatleh _ j1_lt_j2). - rewrite eq in * |-. assert (is_le' : is_leading_entry (mat piv_r) j_2). { unfold is_leading_entry, switch_row in * |-; destruct (stn_eq_or_neq _ _) as [? | ?]; destruct (stn_eq_or_neq _ _) as [? | contr_neq]; simpl in is_le; try apply is_le; simpl in contr_neq; rewrite <- eq in contr_neq; contradiction (isirrefl_natneq _ contr_neq). } unfold is_leading_entry in is_le'. rewrite (pr2 (is_le')); try reflexivity. refine (natlthlehtrans _ _ _ gt j1_lt_j2). 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