Lemma is_Dcuts_corr (X : Dcuts_set) : Dcuts_def_corr (pr1 X). Proof. exact (pr2 (pr2 (pr2 X))). 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.