proposition: Lemma Dcuts_max_lt : ∏ x y z : Dcuts, x < z -> y < z -> Dcuts_max x y < z.
proof: 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.
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