proposition: 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: 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.
imports: UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.Elimination