Definition gauss_clear_column { m n : nat } (mat : Matrix F m n) (k_i : (⟦ m ⟧%stn)) (k_j : (⟦ n ⟧%stn)) (row_sep : ⟦ S m ⟧%stn) : Matrix F m n. Proof. destruct row_sep as [iter lt']. generalize lt'; intros lt; clear lt'. induction iter as [ | iter gauss_clear_column_IH ]. { exact mat. } destruct (natgthorleh iter k_i). 2: {exact mat. } refine (gauss_clear_column_step k_i k_j (iter,, lt) _ ). refine (gauss_clear_column_IH _). now refine (istransnatlth _ _ _ (natgthsnn iter) _). 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.