Definition is_row_echelon {m n : nat} (mat : Matrix R m n) := ∏ i_1 i_2 : ⟦ m ⟧%stn, (∏ j_1 j_2 : ⟦ n ⟧%stn, is_leading_entry (mat i_1) j_1 -> i_1 < i_2 -> j_2 ≤ j_1 -> mat i_2 j_2 = 0%ring) × ((mat i_1 = const_vec 0%ring) -> (i_1 < i_2) -> (mat i_2 = const_vec 0%ring)).
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.