Lemma isboolDcuts_isaprop (x : Dcuts) : isaprop (∏ r, (r ∈ x) ∨ (neg (r ∈ x))). Proof. apply impred_isaprop. intros r. apply pr2. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.