proposition: Lemma Dcuts_lim_cauchy_open : Dcuts_def_open Dcuts_lim_cauchy_val.
proof: Proof. intros r. apply hinhfun ; intros c. exists (r + (pr1 c / 2))%NRat ; split. - apply hinhpr. exists (pr1 c / 2)%NRat ; split. + now apply ispositive_NQhalf, (pr1 (pr2 c)). + exists (pr1 (pr2 (pr2 c))) ; intros n Hn. rewrite isassoc_plusNonnegativeRationals, <- NQhalf_double. now apply (pr2 (pr2 (pr2 c))). - apply plusNonnegativeRationals_lt_r, ispositive_NQhalf. exact (pr1 (pr2 c)). 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