proposition: Lemma Dcuts_half_corr : Dcuts_def_corr Dcuts_half_val.
proof: Proof. intros c Hc. assert (Hc0 : (0 < c + c)%NRat) by (now apply ispositive_plusNonnegativeRationals_l). generalize (X_corr _ Hc0) ; apply hinhfun ; apply sumofmaps ; [intros Hx | intros r]. - left ; exact Hx. - right. exists (pr1 r / 2)%NRat ; split. + unfold Dcuts_half_val. rewrite <- NQhalf_double. exact (pr1 (pr2 r)). + intro H ; apply (pr2 (pr2 r)). apply X_bot with (1 := H). pattern (pr1 r) at 1 ; rewrite (NQhalf_double (pr1 r)), !isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. rewrite iscomm_plusNonnegativeRationals, !isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. rewrite iscomm_plusNonnegativeRationals. now apply isrefl_leNonnegativeRationals. 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