Lemma clear_row_matrix_invertible { m n : nat } (mat : Matrix F m n) (row : (⟦ m ⟧%stn)) (p : n > 0) : @matrix_inverse F _ (gauss_clear_row_as_left_matrix mat row p). Proof. unfold gauss_clear_row_as_left_matrix. destruct (select_uncleared_column F mat row p) as [some | none]. 2: { destruct (natchoice0 m); try apply identity_matrix_invertible; now apply nil_matrix_invertible, identity_matrix_invertible. } apply inv_matrix_prod_invertible. - apply clear_column_matrix_invertible. - apply switch_row_matrix_invertible. 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.