Lemma Dcuts_max_corr : Dcuts_def_corr Dcuts_max_val. Proof. intros c Hc. generalize (X_corr _ Hc) (Y_corr _ Hc) ; apply hinhfun2 ; apply (sumofmaps (Z := _ → _)) ; [intros nXc | intros x] ; apply sumofmaps ; [intros nYc | intros y |intros nYc | intros y]. - left ; unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ; [intros Xc | intros Yc]. + now apply nXc. + now apply nYc. - right. exists (pr1 y) ; split. + apply hinhpr ; right. exact (pr1 (pr2 y)). + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ; [intros Xy | intros Yy]. * now apply nXc, X_bot with (1 := Xy), plusNonnegativeRationals_le_l. * now apply (pr2 (pr2 y)). - right. exists (pr1 x) ; split. + apply hinhpr ; left. exact (pr1 (pr2 x)). + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ; [intros Xx | intros Yx]. * now apply (pr2 (pr2 x)). * now apply nYc, Y_bot with (1 := Yx), plusNonnegativeRationals_le_l. - right. exists (NQmax (pr1 x) (pr1 y)) ; split. + apply NQmax_case. * apply hinhpr ; left. exact (pr1 (pr2 x)). * apply hinhpr ; right. exact (pr1 (pr2 y)). + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps ; [ intros Xxy | intros Yxy]. * apply (pr2 (pr2 x)), X_bot with (1 := Xxy). apply plusNonnegativeRationals_lecompat_r. now apply NQmax_le_l. * apply (pr2 (pr2 y)), Y_bot with (1 := Yxy). apply plusNonnegativeRationals_lecompat_r. now apply NQmax_le_r. 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.