Lemma back_sub_step_inv1 { n : nat } (row : ⟦ n ⟧%stn) (mat : Matrix F n n) (x : Vector F n) (b : Vector F n) : ∏ i : ⟦ n ⟧%stn, i ≠ row -> (col_vec (back_sub_step row mat x b) i = (col_vec x) i). Proof. intros i ne. unfold back_sub_step, col_vec. apply funextfun. intros j; simpl. destruct (nat_eq_or_neq row i) as [eq | ?]; try apply idpath. rewrite eq in ne. contradiction (isirrefl_natneq _ ne). 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.