Lemma leading_entry_compute_inv1 {n : nat} (v : Vector F n) (eq_nothing : (leading_entry_compute v) = nothing) : ∏ i : ⟦ n ⟧%stn, v i = 0%ring. Proof. intros i. rewrite (leading_entry_compute_internal_inv2 _ _ eq_nothing i); try reflexivity. unfold dualelement. destruct (natchoice0 n) as [eq | ?]; simpl. - apply fromstn0; now rewrite eq. - refine (natlehlthtrans (n - 1 - i) (n - 1) n _ _ ). + apply natminuslehn. + now apply natminus1lthn. 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.