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