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