Lemma leading_entry_compute_internal_inv1 {n : nat} (v : Vector F n) (i : ⟦ n ⟧%stn) (eq : (leading_entry_compute_internal v (n,, natgthsnn _)) = (just i)) : is_leading_entry v i. Proof. unfold is_leading_entry. destruct (leading_entry_compute_impl v i eq) as [i' H1]. pose (H2 := leading_entry_compute_eq v i i' eq H1). unfold leading_entry_compute_internal in eq. pose (H3 := @leading_entry_compute_dual_internal_inv4 _ (λ i : (⟦ n ⟧)%stn, v (dualelement i)) (n,, natgthsnn _) (dualelement i)). destruct (maybe_choice' (leading_entry_compute_dual_internal (λ i : (⟦ n ⟧)%stn, v (dualelement i)) (n,, natgthsnn _))) as [t | contr_eq]. 2: { contradiction (@negpathsii1ii2 ((⟦ n ⟧)%stn) unit i' tt). unfold just in H1; rewrite <- H1; now rewrite contr_eq. } destruct t as [t H4], (!H2), H3 as [H5 H6]; try now rewrite dualelement_2x. use tpair; simpl. { now rewrite dualelement_2x in H5. } intros j lt. change 0%ring with (@rigunel1 F) in *. rewrite <- (H6 (dualelement j)). - now rewrite dualelement_2x. - apply dualelement_lt_comp; exact lt. - exact (pr2 (dualelement j)). 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.