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