Lemma Dcuts_half_corr : Dcuts_def_corr Dcuts_half_val. 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.
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.