Lemma clear_column_matrix_invertible { m n : nat } (iter : ⟦ S m ⟧%stn) (mat : Matrix F m n) (k_i : (⟦ m ⟧%stn)) (k_j : stn n) : @matrix_inverse F _ (gauss_clear_column_as_left_matrix iter mat k_i k_j). Proof. unfold gauss_clear_column_as_left_matrix. destruct iter as [iter p]. induction iter as [| iter IH]. { apply identity_matrix_invertible. } rewrite nat_rect_step. destruct (natgthorleh iter k_i). - apply inv_matrix_prod_invertible. { apply add_row_mult_matrix_invertible. now apply natlthtoneq. } apply IH. - apply inv_matrix_prod_invertible. { apply identity_matrix_invertible. } apply IH. 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.