Lemma istrans_Dcuts_eq : istrans Dcuts_eq. Proof. intros x y z Hxy Hyz r. split. - intros Xr. now apply (pr1 (Hyz r)), (pr1 (Hxy r)), Xr. - intros Zr. now apply (pr2 (Hxy r)), (pr2 (Hyz r)), Zr. 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.