Lemma Dcuts_lim_cauchy_open : Dcuts_def_open Dcuts_lim_cauchy_val. 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.
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.