Lemma leading_entry_compute_eq {n : nat} (v : Vector F n) (i_1 i_2 : ⟦ n ⟧%stn) (e_1 : leading_entry_compute v = just i_1) (e_2 : leading_entry_dual_compute (λ i : ⟦ n ⟧%stn, v (dualelement i)) = just i_2) : i_1 = dualelement i_2. Proof. unfold leading_entry_compute, leading_entry_dual_compute, leading_entry_compute_internal in * |-. destruct (leading_entry_compute_dual_internal (λ i : (⟦ n ⟧)%stn, v (dualelement i)) (n,, natgthsnn _)) as [s | contr]. 2: { contradiction (negpathsii1ii2 i_1 tt); apply pathsinv0, e_1. } assert (e_3 : (dualelement s) = i_1). { apply just_injectivity; exact (e_1). } assert (e_4 : s = i_2). { unfold just in e_2; now apply ii1_injectivity in e_2. } now rewrite <- e_3, e_4. 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.