Definition gauss_clear_rows_up_to { m n : nat } (mat : Matrix F m n) (row_sep : (⟦ S m ⟧%stn)) : (Matrix F m n). Proof. destruct row_sep as [row_sep row_sep_lt_n]. induction row_sep as [| row_sep gauss_clear_earlier_rows]. {exact mat. } refine (gauss_clear_row _ (row_sep,, row_sep_lt_n)). refine (gauss_clear_earlier_rows _). exact (istransnatlth _ _ _ (natgthsnn row_sep) row_sep_lt_n ). 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.