Lemma Dcuts_half_open : Dcuts_def_open Dcuts_half_val. Proof. intros r Hr. generalize (X_open _ Hr). apply hinhfun ; intros q. exists (pr1 q / 2)%NRat ; split. - unfold Dcuts_half_val. rewrite <- NQhalf_double. exact (pr1 (pr2 q)). - apply_pr2 (multNonnegativeRationals_ltcompat_l 2%NRat). + exact ispositive_twoNonnegativeRationals. + pattern r at 1 ; rewrite (NQhalf_double r), isldistr_mult_plusNonnegativeRationals, !multdivNonnegativeRationals. * exact (pr2 (pr2 q)). * exact ispositive_twoNonnegativeRationals. * exact ispositive_twoNonnegativeRationals. 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.