proposition: Lemma clear_rows_up_to_as_left_matrix { m n : nat } (mat : Matrix F m n) (row_sep : (⟦ S m ⟧%stn)) (p : n > 0) : (Matrix F m m).
proof: Proof. destruct row_sep as [row_sep row_sep_lt_n]. induction row_sep as [ | row_sep gauss_clear_earlier_rows]. { exact (@identity_matrix F m). } assert (lt : row_sep < S m). { apply (istransnatlth _ _ _ (natgthsnn row_sep) row_sep_lt_n ). } set (mat_by_normal_op := (gauss_clear_rows_up_to mat (row_sep,, lt))). refine ((gauss_clear_row_as_left_matrix mat_by_normal_op (row_sep,, row_sep_lt_n) p ** _)). exact (gauss_clear_earlier_rows lt). 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