proposition: Lemma gauss_clear_rows_up_to_inv1 { m n : nat } (mat : Matrix F m n) (p : n > 0) (row_sep : (⟦ S m ⟧%stn)) : is_row_echelon_partial_1 (gauss_clear_rows_up_to mat row_sep) row_sep.
proof: Proof. unfold gauss_clear_rows_up_to. destruct row_sep as [row_sep p'']. induction row_sep as [| row_sep IH]. { simpl; intros ? ? ? ? contr; contradiction (negnatlthn0 n contr). } rewrite nat_rect_step. set (inner := nat_rect _ _ _ _). set (lt' := (istransnatlth _ _ _ (natgthsnn row_sep) p'')). apply (gauss_clear_row_inv0 (inner lt') p (row_sep,, lt') _), IH. 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