Lemma Dcuts_max_lt : ∏ x y z : Dcuts, x < z -> y < z -> Dcuts_max x y < z. Proof. intros x y z. apply hinhfun2 ; intros rx ry. exists (NQmax (pr1 rx) (pr1 ry)) ; split. - apply NQmax_case_strong ; intro Hr. + intro Hr' ; apply (pr1 (pr2 ry)). revert Hr' ; apply hinhuniv ; apply sumofmaps ; [ intros Xr | intros Yr]. * now apply fromempty, (pr1 (pr2 rx)). * now apply is_Dcuts_bot with (1 := Yr). + intro Hr' ; apply (pr1 (pr2 rx)). revert Hr' ; apply hinhuniv ; apply sumofmaps ; [intros Xr | intros Yr]. * now apply is_Dcuts_bot with (1 := Xr). * now apply fromempty, (pr1 (pr2 ry)). - apply NQmax_case. + exact (pr2 (pr2 rx)). + exact (pr2 (pr2 ry)). 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.