proposition: Lemma leading_entry_compute_internal_inv2 {n : nat} (v : Vector F n) (iter : ⟦ S n ⟧%stn) (eq_nothing : (leading_entry_compute_internal v iter) = nothing) : ∏ i : ⟦ n ⟧%stn, (dualelement i) < iter -> v i = 0%ring.
proof: Proof. intros i i_lt_iter. revert eq_nothing. unfold leading_entry_compute_internal, leading_entry_compute_dual_internal. destruct iter as [iter pr2_]. induction iter as [| iter IH]. - now apply negnatlthn0 in i_lt_iter. - rewrite nat_rect_step. destruct (fldchoice0 _) as [? | _]. 2 : { simpl; unfold just; intros contr. apply negpathsii1ii2 in contr. now apply fromempty. } destruct (natlehchoice (dualelement i) (iter)). { now apply natlthsntoleh. } + now apply IH. + intros ?. rewrite (dualelement_eq i (iter,, pr2_)); try easy. now apply subtypePath_prop. 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