proposition: Lemma is_row_echelon_from_partial {m n : nat} (mat : Matrix F m n) : (is_row_echelon_partial mat (m,, natgthsnn _)) -> is_row_echelon mat.
proof: Proof. unfold is_row_echelon, is_row_echelon_partial. unfold is_row_echelon_partial_1, is_row_echelon_partial_2. intros H ? ?; intros; use tpair. { intros j_1 j_2 X. refine (pr1 H i_1 i_2 j_2 _ _ _ ); try apply X; try assumption; exact (pr2 i_1). } simpl; intros. refine ((pr2 H) i_1 i_2 _ _ _ ); try assumption. exact (pr2 i_1). 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