Lemma select_uncleared_column_internal {m n : nat} (mat : Matrix F m n) (row_sep : ⟦ m ⟧%stn) (col_iter : ⟦ S n ⟧%stn) (p : n > 0) : coprod (exists_first_uncleared mat row_sep col_iter) (lower_left_zero mat row_sep col_iter). Proof. destruct (natchoice0 m) as [contr_eq | _]. { apply fromstn0; now rewrite contr_eq. } destruct col_iter as [col_iter lt]. induction col_iter as [| col_iter IH]. { right; intros ? _ ? contr. contradiction (negnatgth0n n contr). } assert (lt' : col_iter < S n). { simpl in lt. apply (istransnatlth _ _ _ lt (natgthsnn n)). } destruct (IH lt') as [IH_left | IH_right]. - destruct IH_left as [m' [H1 [H2 H3]]]. left; exists m', (istransnatlth _ _ _ H1 (natgthsnn col_iter)), H2. apply H3. - destruct (select_pivot_row_coprod mat row_sep (col_iter,, lt)) as [nz | z]. + left; exists (col_iter,, lt) , (natgthsnn col_iter); do 3 (use tpair; try apply nz); simpl; intros; now apply IH_right. + right. intros i rowsep_le_i j j_lt_scoliter. destruct (natlehchoice j col_iter) as [? | eq]; intros. { apply (natlehlthtrans _ _ _ j_lt_scoliter). apply (natgthsnn col_iter). } { now apply IH_right. } rewrite <- (z i); try assumption. now apply maponpaths, subtypePath_prop. 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.