proposition: 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: 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.
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