Definition Dcuts_inv (X : Dcuts) (X_0 : X ≠ 0) : Dcuts. Proof. intros. apply (make_Dcuts (Dcuts_inv_val (pr1 X))). - now apply Dcuts_inv_bot. - apply Dcuts_inv_open. + now apply is_Dcuts_bot. + now apply Dcuts_def_corr_finite, is_Dcuts_corr. - apply Dcuts_inv_corr. + now apply is_Dcuts_bot. + now apply is_Dcuts_open. + now apply is_Dcuts_corr. + now apply_pr2 Dcuts_apzero_notempty. 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.