proposition: Lemma row_echelon_to_upper_triangular { m n : nat } (mat : Matrix F m n) : is_row_echelon mat -> @is_upper_triangular F _ _ mat.
proof: 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.
imports: UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.MoreFoundations.Tactics UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices UniMath.Algebra.GaussianElimination.Elimination