Lemma Dcuts_notlt_0 : ∏ x : Dcuts, ¬ (x < Dcuts_zero). Proof. intros x. unfold neg. apply factor_through_squash. - exact isapropempty. - intros r. exact (Dcuts_zero_empty _ (pr2 (pr2 r))). 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.