Definition select_pivot_row_coprod {m n : nat} (mat : Matrix F m n) (row_sep : ⟦ m ⟧%stn) (k : ⟦ n ⟧%stn) : coprod ((∑ i: ⟦ m ⟧%stn, row_sep ≤ i × ((mat i k) != 0%ring))) (∏ i : ⟦ m ⟧%stn, row_sep ≤ i -> mat i k = 0%ring). Proof. pose (H := (@leading_entry_compute_dual_internal_inv1 _ _ (col mat k) (m,, natgthsnn _))). destruct (maybe_choice' (leading_entry_compute_dual_internal _ (col mat k) (m,, natgthsnn _))) as [some | none]. - destruct some as [t ist]. destruct (H t) as [lt neq0]; try assumption. destruct (natlthorgeh t row_sep) as [? | gt]. 2: { apply ii1; exists t, gt; apply neq0. } apply ii2. destruct (@leading_entry_compute_dual_internal_inv4 _ _ (col mat k) (m,, natgthsnn _) t ist) as [H3 H4]. intros i ke_le_i. unfold col, transpose, flip in * |-. rewrite H4; try easy; try now apply (natlthlehtrans _ row_sep i). exact (pr2 i). - apply ii2; intros. pose (H' := @leading_entry_compute_dual_internal_inv2). rewrite <- (H' _ _ (col mat k) (m,, natgthsnn _) none i); try reflexivity. apply (pr2 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.