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