proposition: Lemma Dcuts_plus_lt_l : ∏ x x' y : Dcuts, Dcuts_plus x y < Dcuts_plus x' y -> x < x'.
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals