Lemma leading_entry_compute_inv2 {n : nat} (v : Vector F n) (i : ⟦ n ⟧%stn) (eq : (leading_entry_compute v) = just i) : is_leading_entry v i. Proof. use tpair; simpl. { now apply leading_entry_compute_internal_inv1. } intros i' i_gt_i'. destruct (@leading_entry_compute_impl _ _ _ eq) as [entry compeq]. pose (H := @leading_entry_compute_dual_internal_inv4 _ _ _ _ compeq). simpl in H; destruct H as [neq0 eq0]. rewrite <- (eq0 (dualelement i')). - now rewrite dualelement_2x. - apply dualelement_lt_comp'. rewrite dualelement_2x. rewrite <- (@leading_entry_compute_eq _ _ _ entry eq compeq). exact i_gt_i'. - exact (pr2 (dualelement i')). 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.