Lemma back_sub_step_inv2 { n : nat } (row : ⟦ n ⟧%stn) (mat : Matrix F n n) (x : Vector F n) (b : Vector F n) (is_ut: @is_upper_triangular F n n mat) : ∏ i : ⟦ n ⟧%stn, i ≥ row -> (mat i i != 0)%ring -> (mat ** (col_vec x)) i = (col_vec b) i -> (mat ** (col_vec (back_sub_step row mat x b))) i = (col_vec b) i. Proof. unfold transpose, flip. intros i le neq0 H. rewrite <- H. destruct (natlehchoice row i) as [lt | eq]. {apply le. } - rewrite matrix_mult_eq in *. apply pathsinv0. rewrite matrix_mult_eq. unfold matrix_mult_unf in *. apply funextfun; intros ?. apply maponpaths, funextfun; intros i'. destruct (stn_eq_or_neq i' (row)) as [eq | neq]. 2 : { now rewrite back_sub_step_inv1. } rewrite is_ut. 2: { rewrite eq. assumption. } do 2 rewrite (@rigmult0x F). apply idpath. - rewrite (stn_eq _ _ eq) , back_sub_step_inv0; try assumption. now rewrite H. 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.