Definition leading_entry_compute_dual_internal_inv2 {n : nat} (v : Vector F n) (iter : ⟦ S n ⟧%stn) (not_nothing : (leading_entry_compute_dual_internal v iter) = nothing) : ∏ i : ⟦ n ⟧%stn, i < iter -> v i = 0%ring. Proof. intros i i_lt_iter. revert not_nothing. unfold leading_entry_compute_dual_internal. destruct iter as [iter p]. induction iter as [| iter IH]. { apply fromempty; now apply negnatlthn0 in i_lt_iter. } rewrite nat_rect_step. destruct (fldchoice0 (v (iter,, p))) as [eq0 | ?]. 2 : { intros contr; now apply negpathsii1ii2 in contr. } destruct (natlehchoice i iter) as [le | eq]. {now apply natlthsntoleh. } - intros H; now apply IH in H. - intros ?; refine (_ @ eq0); apply maponpaths, stn_eq, eq. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSequences. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices. Require Import UniMath.Algebra.GaussianElimination.RowOps.