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