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