Definition leading_entry_compute_dual_internal_general {X : UU} { n : nat } (v : Vector F n) (iter : ⟦ S n ⟧%stn) : maybe (⟦ n ⟧%stn). Proof. destruct iter as [iter lt]. induction iter as [| iter IH]. { exact nothing. } simpl in lt. destruct (fldchoice0 (v (iter,, lt))). - refine (IH _); apply (istransnatlth _ _ _ lt (natgthsnn n)). - exact (just (iter,, lt)). 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.