Lemma isirrefl_Dcuts_lt_rel : isirrefl Dcuts_lt_rel. Proof. intros x. unfold neg ; apply (hinhuniv (P := make_hProp _ isapropempty)). intros r. apply (pr1 (pr2 r)). exact (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.