Lemma gauss_clear_column_inv2 { m n : nat } (k_i : (⟦ m ⟧%stn)) (k_j : stn n) (row_sep : ⟦ S m ⟧%stn) (mat : Matrix F m n) : ∏ r : (⟦ m ⟧%stn), r < row_sep -> k_i < r -> ((gauss_clear_column mat k_i k_j row_sep) r = (gauss_clear_column_step' k_i k_j r mat) r). Proof. unfold gauss_clear_column. destruct row_sep as [sep p]. induction sep as [| sep IH]. { intros r r_le_0. contradiction (negnatgth0n r r_le_0). } intros r r_le_sn k_le_r. set (p' := istransnatlth _ _ _ (natgthsnn _) p). destruct (natlehchoice r sep) as [lt | eq]. {assumption. } - assert (le: r ≤ sep). { now apply natlthtoleh in lt. } unfold gauss_clear_column. rewrite nat_rect_step. unfold gauss_clear_column in IH. destruct (natgthorleh _ _) as [le' | gt]. + rewrite (gauss_clear_column_step_inv2). 2 : { apply natgthtoneq in lt; apply issymm_natneq; apply lt. } now rewrite <- (IH p'). + assert (absurd : sep ≤ r). * apply natgthtogeh in k_le_r. apply (istransnatleh gt k_le_r). * now apply natgehtonegnatlth in absurd. - rewrite nat_rect_step. unfold gauss_clear_column_step'. destruct (natgthorleh _ _) as [gt | leh]. 2 : { unfold gauss_clear_column_step. destruct (stn_eq_or_neq _ _); try reflexivity. assert (absurd : sep ≤ r). { apply natgthtogeh in k_le_r. rewrite eq; apply isreflnatgeh. } destruct (!eq). now apply natlehneggth in leh. } destruct (stn_eq_or_neq _ _) as [contr_eq | ?]. { rewrite contr_eq in k_le_r. contradiction (isirreflnatgth _ k_le_r). } assert (interchange : gauss_clear_column_step k_i k_j (sep,, p) (gauss_clear_column mat k_i k_j (sep,, p')) r = gauss_clear_column (gauss_clear_column_step k_i k_j (sep,, p) mat) k_i k_j (sep,, p') r). { do 2 rewrite gauss_clear_column_step_eq. unfold gauss_clear_column_step'. destruct (stn_eq_or_neq _ _); try reflexivity. unfold add_row_mult. rewrite gauss_clear_column_inv0; simpl; try apply natlthnsn. generalize p; generalize p'; rewrite <- eq; intros q q'; simpl. destruct (stn_eq_or_neq _ _) as [? | contr_neq]; simpl. 2: { contradiction (isirrefl_natneq _ contr_neq). } etrans. 2: { rewrite (gauss_clear_column_inv0); try reflexivity; simpl. rewrite eq; apply natlthnsn. } destruct (stn_eq_or_neq _ _) as [? | contr_neq]; simpl. 2: { contradiction (isirrefl_natneq _ contr_neq). } apply funextfun; intros y. apply maponpaths, maponpaths_12. - do 2 apply maponpaths. rewrite gauss_clear_column_inv1. {reflexivity. } apply isreflnatgeh. - rewrite gauss_clear_column_inv1; try reflexivity; apply isreflnatleh. } pose (@gauss_clear_column_inv0 m n k_i k_j (sep,, p')) as p1. change (istransnatlth _ _ _ (natgthsnn _) p) with p'. rewrite <- (stn_eq_2 _ _ eq p) in interchange |- *. do 2 rewrite gauss_clear_column_step_eq in interchange. rewrite gauss_clear_column_step_eq in *; unfold gauss_clear_column_step' in *. destruct (stn_eq_or_neq _ _) as [contr_eq | ?]; try reflexivity. { rewrite contr_eq in k_le_r; contradiction (isirreflnatgth _ k_le_r). } unfold gauss_clear_column in interchange, p1 |-; rewrite interchange. rewrite p1; rewrite (stn_eq_2 _ _ eq p); now try apply isreflnatleh. 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.