proposition: Lemma Dcuts_half_open : Dcuts_def_open Dcuts_half_val.
proof: 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.
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