Proposition trans_dcpo {X : dcpo} {x y z : X} (p : x ⊑ y) (q : y ⊑ z) : x ⊑ z. Proof. exact (trans_PartialOrder X p q). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.