Definition leading_entry_compute_dual_internal_inv3 {n : nat} (v : Vector F n) (iter : ⟦ S n ⟧%stn) (i : ⟦ n ⟧%stn) (eq : (leading_entry_compute_dual_internal v iter) = just i) : (∏ i' : ⟦ n ⟧%stn, i < i' -> i' < iter -> v i' = 0%ring). Proof. revert eq. destruct iter as [iter p]. induction iter as [| iter IH]. { intros _ ? _ x; contradiction (negnatgth0n _ x). } set (p' := istransnatlth iter _ _ p (natgthsnn _)). pose (@leading_entry_compute_dual_internal n v (S _,, p)) as H. destruct (maybe_choice' H) as [s | c]. 2: {unfold H in c; intros; rewrite eq in c; contradiction (negpathsii1ii2 _ _ c). } unfold leading_entry_compute_dual_internal; rewrite nat_rect_step. destruct (fldchoice0 (v (iter,, p) )) as [z | nz]. - intros H'. simpl; intros i' ? ?. destruct (natlehchoice i' iter) as [? | eq']. {assumption. } 2: {refine (_ @ z); apply maponpaths, stn_eq, eq'. } apply (IH p'); try assumption. - intros ? j i_le_iter lts. apply natlthtonegnatgeh in i_le_iter. unfold leading_entry_compute_dual_internal in eq. apply just_injectivity in eq. now rewrite <- eq in * |-. 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.