proposition: Lemma NonnegativeRationals_to_Dcuts_notin_le : ∏ (x : Dcuts) (r : NonnegativeRationals), ¬ (r ∈ x) -> x <= NonnegativeRationals_to_Dcuts r.
proof: Proof. intros x r Hr q Hq. simpl. now apply (Dcuts_finite x). Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals