Definition Dcuts_lim_cauchy_seq (U : nat → Dcuts) (HU : Dcuts_Cauchy_seq U) : Dcuts. Proof. exists (Dcuts_lim_cauchy_val (λ n, pr1 (U n))). repeat split. - apply Dcuts_lim_cauchy_bot. intro ; now apply is_Dcuts_bot. - apply Dcuts_lim_cauchy_open. - apply Dcuts_lim_cauchy_corr. + intro ; now apply is_Dcuts_bot. + intro ; now apply is_Dcuts_corr. + intros eps Heps. assert (X : 0 < NonnegativeRationals_to_Dcuts eps) by (now apply_pr2 isapfun_NonnegativeRationals_to_Dcuts_aux). generalize (HU _ X) ; clear HU. apply hinhfun ; intros HU. exists (pr1 HU) ; intros n m Hn Hm. set (pr2 HU n m Hn Hm) ; clearbody d ; clear -d ; rename d into HU. split. * now refine (Dcuts_lt_le_rel _ _ (pr1 HU)). * now refine (Dcuts_lt_le_rel _ _ (pr2 HU)). Defined.
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.