Lemma leading_entry_compute_internal_inv2 {n : nat} (v : Vector F n) (iter : ⟦ S n ⟧%stn) (eq_nothing : (leading_entry_compute_internal v iter) = nothing) : ∏ i : ⟦ n ⟧%stn, (dualelement i) < iter -> v i = 0%ring. Proof. intros i i_lt_iter. revert eq_nothing. unfold leading_entry_compute_internal, leading_entry_compute_dual_internal. destruct iter as [iter pr2_]. induction iter as [| iter IH]. - now apply negnatlthn0 in i_lt_iter. - rewrite nat_rect_step. destruct (fldchoice0 _) as [? | _]. 2 : { simpl; unfold just; intros contr. apply negpathsii1ii2 in contr. now apply fromempty. } destruct (natlehchoice (dualelement i) (iter)). { now apply natlthsntoleh. } + now apply IH. + intros ?. rewrite (dualelement_eq i (iter,, pr2_)); try easy. now apply subtypePath_prop. 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.