Lemma Dcuts_minus_corr : Dcuts_def_corr Dcuts_minus_val. Proof. assert (Y_corr' : Dcuts_def_corr (λ y, Y y ∨ (y = 0%NRat))). { intros c Hc. generalize (Y_corr c Hc) ; apply hinhfun ; apply sumofmaps ; [intros Yc | intros y ]. - left. intros H ; apply Yc ; clear Yc ; revert H. apply hinhuniv ; apply sumofmaps ; [intros Yc | intros Hc0]. + exact Yc. + rewrite Hc0 in Hc. now apply fromempty, (isirrefl_ltNonnegativeRationals 0%NRat). - right. exists (pr1 y) ; split. + apply hinhpr ; left. exact (pr1 (pr2 y)). + intros H ; apply (pr2 (pr2 y)) ; revert H. apply hinhuniv ; apply sumofmaps ; [intros H | intros Hc0]. * exact H. * apply fromempty ; revert Hc0. apply gtNonnegativeRationals_noteq. now apply ispositive_plusNonnegativeRationals_r. } intros c Hc. apply ispositive_NQhalf in Hc. apply (λ X X0 Xerr, Dcuts_def_corr_not_empty X X0 Xerr _ Hc) in Y_corr'. - revert Y_corr' ; apply hinhuniv ; intros y. generalize (pr1 (pr2 y)) ; apply hinhuniv ; intros Yy. assert (X0 : ¬ Y (pr1 y + c / 2%NRat)). { intro ; apply (pr2 (pr2 y)). now apply hinhpr ; left. } rename X0 into nYy. generalize (X_corr _ Hc) ; apply hinhuniv ; apply sumofmaps ; [intros Xc | intros x]. + apply hinhpr ; left ; intro H ; apply Xc. revert H ; apply hinhuniv ; intros x. apply X_bot with (1 := pr1 (pr2 x)). apply istrans_leNonnegativeRationals with c. * pattern c at 2 ; rewrite (NQhalf_double c). now apply plusNonnegativeRationals_le_r. * apply lt_leNonnegativeRationals. pattern c at 1 ; rewrite <- (isrunit_zeroNonnegativeRationals c). apply (pr2 (pr2 x)). now right. + generalize (isdecrel_leNonnegativeRationals (pr1 y + c / 2)%NRat (pr1 x)) ; apply sumofmaps ; intro Hxy. * assert (HY : ∏ y', (Y y') ⨿ (y' = 0%NRat) -> (y' < pr1 y + c / 2)%NRat). { intros y' ; apply sumofmaps ; intros Yy'. - apply notge_ltNonnegativeRationals ; intro H ; apply nYy. now apply Y_bot with (1 := Yy'). - rewrite Yy'. now apply ispositive_plusNonnegativeRationals_r. } apply hinhpr ; right ; exists (pr1 x - (pr1 y + c / 2))%NRat ; split. ** apply hinhpr. exists (pr1 x) ; split. *** exact (pr1 (pr2 x)). *** intros y' Yy'. pattern (pr1 x) at 2 ; rewrite <- (minusNonnegativeRationals_plus_r _ _ Hxy). apply plusNonnegativeRationals_ltcompat_l. now apply HY. ** unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros x'. generalize (pr2 (pr2 x') (pr1 y) Yy). apply_pr2 notlt_geNonnegativeRationals. apply istrans_leNonnegativeRationals with (pr1 x + c / 2)%NRat. *** apply lt_leNonnegativeRationals. apply notge_ltNonnegativeRationals ; intro H ; apply (pr2 (pr2 x)). now apply X_bot with (1 := pr1 (pr2 x')). *** rewrite isassoc_plusNonnegativeRationals, (iscomm_plusNonnegativeRationals _ (pr1 y)). pattern c at 3; rewrite (NQhalf_double c). rewrite <- (isassoc_plusNonnegativeRationals (pr1 y)), <- isassoc_plusNonnegativeRationals. rewrite minusNonnegativeRationals_plus_r. **** apply isrefl_leNonnegativeRationals. **** exact Hxy. * apply notge_ltNonnegativeRationals in Hxy. apply hinhpr ; left ; unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; intros x'. generalize (pr2 (pr2 x') _ Yy). apply_pr2 notlt_geNonnegativeRationals. induction (isdecrel_leNonnegativeRationals (pr1 y) (pr1 x')) as [Hxy' | Hxy']. ** rewrite iscomm_plusNonnegativeRationals. pattern c at 1; rewrite (NQhalf_double c), <- isassoc_plusNonnegativeRationals. apply istrans_leNonnegativeRationals with (pr1 x + c / 2)%NRat. *** apply lt_leNonnegativeRationals ; apply notge_ltNonnegativeRationals ; intro ; apply (pr2 (pr2 x)). now apply X_bot with (1 := pr1 (pr2 x')). *** apply plusNonnegativeRationals_lecompat_r. now apply lt_leNonnegativeRationals. ** apply notge_ltNonnegativeRationals in Hxy'. apply istrans_leNonnegativeRationals with (pr1 y). *** now apply lt_leNonnegativeRationals. *** now apply plusNonnegativeRationals_le_l. - now apply hinhpr ; right. 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.