Lemma isstpo_Dcuts_lt_rel : isStrongOrder Dcuts_lt_rel. Proof. repeat split. - exact istrans_Dcuts_lt_rel. - exact iscotrans_Dcuts_lt_rel. - exact isirrefl_Dcuts_lt_rel. 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.