proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSequences UniMath.Combinatorics.Vectors UniMath.Combinatorics.Maybe UniMath.Algebra.BinaryOperations UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.RigsAndRings UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.RowOps