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