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