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