Lemma back_sub_internal_inv2 { n : nat } (mat : Matrix F n n) (x : Vector F n) (b : Vector F n) (ut : @is_upper_triangular F _ _ mat) (sep : ⟦ S n ⟧%stn) (row : ⟦ S n ⟧%stn) : ∏ (i : ⟦ n ⟧%stn), i ≥ (dualelement sep) -> (mat i i != 0)%ring -> i < row -> (mat ** (col_vec (back_sub_internal mat x b sep row))) i = (col_vec b) i. Proof. unfold transpose, flip. intros i i_le_sep neq0 lt. unfold back_sub_internal. destruct sep as [sep p]. induction sep as [| sep IH]. { apply fromempty, (dualelement_sn_stn_nge_0 _ _ i_le_sep). } rewrite nat_rect_step. destruct (natlehchoice (dualelement (sep,, p)) i) as [leh | eq]. { refine (istransnatleh _ i_le_sep). now apply (@dualelement_sn_le). } - destruct (natlthorgeh _ _) as [? | contr_geh]. 2 : { contradiction (isirreflnatlth _ (natlthlehtrans _ _ _ (istransnatlth _ _ _ leh lt) contr_geh)). } rewrite back_sub_step_inv2; try easy. { unfold dualelement. unfold dualelement in leh. destruct (natchoice0 _) as [contr_eq | ?]. {apply fromstn0. now rewrite contr_eq. } now apply natgthtogeh. } rewrite IH; try reflexivity. now apply dualelement_lt_to_le_s. - destruct (natlthorgeh _ _) as [? | contr_geh]. + rewrite (stn_eq _ _ eq). now rewrite back_sub_step_inv0. + rewrite <- (stn_eq _ _ eq) in lt. contradiction (isirreflnatlth _ (natlthlehtrans _ _ _ lt contr_geh)). Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices. Require Import UniMath.Algebra.GaussianElimination.Elimination.