Lemma Dcuts_plus_lt_l : ∏ x x' y : Dcuts, Dcuts_plus x y < Dcuts_plus x' y -> x < x'. Proof. intros x x' y. apply hinhuniv ; intros r. generalize (pr2 (pr2 r)) ; apply hinhfun ; apply sumofmaps ; [ apply sumofmaps ; [ intros Xr | intros Yr] | intros xy ]. - exists (pr1 r) ; split. + intro H ; apply (pr1 (pr2 r)). now apply hinhpr ; left ; left. + exact Xr. - apply fromempty, (pr1 (pr2 r)). now apply hinhpr ; left ; right. - exists (pr1 (pr1 xy)) ; split. + intro H ; apply (pr1 (pr2 r)). apply hinhpr ; right ; exists (pr1 xy). repeat split. * exact (pr1 (pr2 xy)). * exact H. * exact (pr2 (pr2 (pr2 xy))). + exact (pr1 (pr2 (pr2 xy))). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.