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