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