Lemma row_echelon_to_upper_triangular { m n : nat } (mat : Matrix F m n) : is_row_echelon mat -> @is_upper_triangular F _ _ mat. Proof. destruct (natchoice0 n) as [contr_eq0 | p]. { intros ? ? j; apply fromstn0; now rewrite contr_eq0. } intros H; unfold is_upper_triangular; intros. rewrite (row_echelon_partial_to_upper_triangular_partial mat p (m,, natgthsnn _)) ; try easy. 2: {exact (pr2 i). } use tpair; intros i_1 i_2 j_1 j_2; intros; simpl. - destruct (H i_1 i_2) as [H1 _]; now rewrite (H1 j_2 j_1). - destruct (H i_1 i_2) as [_ H2]; now rewrite H2. Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices. Require Import UniMath.Algebra.GaussianElimination.Elimination.