Lemma gauss_clear_rows_up_to_as_matrix_eq { m n : nat } (iter : ⟦ S m ⟧%stn) (mat : Matrix F m n) (p : n > 0) : ((@clear_rows_up_to_as_left_matrix _ _ mat iter p) ** mat) = (gauss_clear_rows_up_to mat iter). Proof. intros. unfold clear_rows_up_to_as_left_matrix, gauss_clear_rows_up_to, clear_rows_up_to_as_left_matrix, gauss_clear_rows_up_to. destruct iter as [iter ?]. induction iter as [| iter IH ]. {simpl; now rewrite matlunax2. } do 2 rewrite nat_rect_step, <- IH. now rewrite <- (clear_row_eq_matrix_def _ _ p), <- matrix_mult_assoc. 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.