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