proposition: 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: 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.
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