Lemma leading_entry_compute_dual_internal_inv1 { n : nat } (v : Vector F n) (iter : ⟦ S n ⟧%stn) {i : stn n} (not_nothing : (leading_entry_compute_dual_internal v iter) = just i) : i < iter × (v i != 0%ring). Proof. revert not_nothing. unfold leading_entry_compute_dual_internal. destruct iter as [iter p]. induction iter as [| iter IH]. { simpl; intros. contradiction (negpathsii1ii2 _ _ (!not_nothing)). } rewrite nat_rect_step. destruct (fldchoice0 _) as [eq0| neq0]. - intros H; apply IH in H; destruct H as [lt neq0]. use tpair. {apply (istransnatlth _ _ _ lt (natgthsnn iter) ). } apply neq0. - intros ?. rename not_nothing into eq; apply just_injectivity in eq. use tpair. {rewrite <- eq. apply natgthsnn. } rewrite <- eq; exact neq0. 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.