proposition: Lemma gauss_clear_rows_up_to_matrix_invertible {m n : nat} (iter : ⟦ S m ⟧%stn) (mat : Matrix F m n) (p : n > 0) : @matrix_inverse F _ (clear_rows_up_to_as_left_matrix mat iter p).
proof: Proof. unfold clear_rows_up_to_as_left_matrix. set (pre := gauss_clear_column_as_left_matrix iter mat ). unfold gauss_clear_column_as_left_matrix in pre. destruct iter as [iter lt]. induction iter as [| ? IH]. - simpl. apply identity_matrix_invertible. - unfold clear_rows_up_to_as_left_matrix. rewrite nat_rect_step. apply inv_matrix_prod_invertible. + now apply clear_row_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