Lemma Dcuts_plus_corr : Dcuts_def_corr Dcuts_plus_val. Proof. intros c Hc. apply ispositive_NQhalf in Hc. generalize (X_corr _ Hc) (Y_corr _ Hc). apply hinhfun2 ; apply (sumofmaps (Z := _ → _)) ; intros Hx ; apply sumofmaps ; intros Hy. - left. unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps. + apply sumofmaps ; intros Hz. * apply Hx. apply X_bot with (1 := Hz). pattern c at 2 ; rewrite (NQhalf_double c). apply plusNonnegativeRationals_le_r. * apply Hy. apply Y_bot with (1 := Hz). pattern c at 2 ; rewrite (NQhalf_double c). apply plusNonnegativeRationals_le_r. + intros xy. generalize (isdecrel_ltNonnegativeRationals (pr1 (pr1 xy)) (c / 2)%NRat) ; apply sumofmaps ; intros Hx'. * generalize (isdecrel_ltNonnegativeRationals (pr2 (pr1 xy)) (c / 2)%NRat) ; apply sumofmaps ; intros Hy'. ** apply (isirrefl_isStrongOrder ltNonnegativeRationals c). pattern c at 2 ; rewrite (NQhalf_double c). pattern c at 1 ; rewrite (pr1 (pr2 xy)). apply plusNonnegativeRationals_ltcompat. *** exact Hx'. *** exact Hy'. ** apply Hy. apply Y_bot with (1 := pr2 (pr2 (pr2 xy))). now apply notlt_geNonnegativeRationals ; apply Hy'. * apply Hx. apply X_bot with (1 := pr1 (pr2 (pr2 xy))). now apply notlt_geNonnegativeRationals ; apply Hx'. - right. rename Hy into q. exists (pr1 q) ; split. + apply hinhpr. left ; right ; exact (pr1 (pr2 q)). + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps. * apply sumofmaps ; [intros Xq | intros Yq']. ** apply Hx ; apply X_bot with (1 := Xq). pattern c at 2; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_le_l. ** apply (pr2 (pr2 q)) ; apply Y_bot with (1 := Yq'). pattern c at 2; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_le_r. * intros xy. apply (isirrefl_isStrongOrder ltNonnegativeRationals (pr1 q + c)). pattern c at 2; rewrite (NQhalf_double c). pattern (pr1 q + c) at 1 ; rewrite (pr1 (pr2 xy)). rewrite <- isassoc_plusNonnegativeRationals. rewrite iscomm_plusNonnegativeRationals. apply plusNonnegativeRationals_ltcompat. ** apply notge_ltNonnegativeRationals ; intro H. apply (pr2 (pr2 q)) ; apply Y_bot with (1 := pr2 (pr2 (pr2 xy))). exact H. ** apply notge_ltNonnegativeRationals ; intro H. apply Hx ; apply X_bot with (1 := pr1 (pr2 (pr2 xy))). exact H. - right. rename Hx into q. exists (pr1 q) ; split. + apply hinhpr. left ; left ; exact (pr1 (pr2 q)). + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps. * apply sumofmaps ; [intros Xq' | intros Yq]. ** apply (pr2 (pr2 q)) ; apply X_bot with (1 := Xq'). pattern c at 2; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_le_r. ** apply Hy ; apply Y_bot with (1 := Yq). pattern c at 2; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_le_l. * intros xy. apply (isirrefl_isStrongOrder ltNonnegativeRationals (pr1 q + c)). pattern c at 2; rewrite (NQhalf_double c). pattern (pr1 q + c) at 1 ; rewrite (pr1 (pr2 xy)). rewrite <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_ltcompat. ** apply notge_ltNonnegativeRationals ; intro H. apply (pr2 (pr2 q)) ; apply X_bot with (1 := pr1 (pr2 (pr2 xy))). exact H. ** apply notge_ltNonnegativeRationals ; intro H. apply Hy ; apply Y_bot with (1 := pr2 (pr2 (pr2 xy))). exact H. - right. rename Hx into qx ; rename Hy into qy. exists (pr1 qx + pr1 qy). split. + apply hinhpr. right. exists (pr1 qx,,pr1 qy) ; repeat split. * exact (pr1 (pr2 qx)). * exact (pr1 (pr2 qy)). + unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)) ; apply sumofmaps. * apply sumofmaps ; [ intros Xq' | intros Yq']. ** apply (pr2 (pr2 qx)), X_bot with (1 := Xq'). pattern c at 2; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_r. rewrite isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_le_r. ** apply (pr2 (pr2 qy)), Y_bot with (1 := Yq'). pattern c at 2; rewrite (NQhalf_double c). rewrite <- isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_r. eapply istrans_leNonnegativeRationals, plusNonnegativeRationals_le_r. apply plusNonnegativeRationals_le_l. * intros xy. apply (isirrefl_isStrongOrder ltNonnegativeRationals (pr1 qx + pr1 qy + c)). pattern c at 2; rewrite (NQhalf_double c). pattern (pr1 qx + pr1 qy + c) at 1 ; rewrite (pr1 (pr2 xy)). rewrite <- isassoc_plusNonnegativeRationals. rewrite (isassoc_plusNonnegativeRationals (pr1 qx) (pr1 qy) (c / 2)%NRat). rewrite (iscomm_plusNonnegativeRationals (pr1 qy)). rewrite <- isassoc_plusNonnegativeRationals. rewrite (isassoc_plusNonnegativeRationals (pr1 qx + (c/2)%NRat)). apply plusNonnegativeRationals_ltcompat. ** apply notge_ltNonnegativeRationals ; intro H. apply (pr2 (pr2 qx)) ; apply X_bot with (1 := pr1 (pr2 (pr2 xy))) ; exact H. ** apply notge_ltNonnegativeRationals ; intro H. apply (pr2 (pr2 qy)) ; apply Y_bot with (1 := pr2 (pr2 (pr2 xy))) ; exact H. 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.