proposition: Lemma isaset_boolDcuts : isaset isboolDcuts.
proof: Proof. apply isasetsubset with pr1. - apply pr2. - apply isinclpr1. intro x. apply pr2. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals