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