Proposition trans_le_way_below {x y z : X} (p : x ⊑ y) (q : y ≪ z) : x ≪ z. Proof. intros D HD. assert (H := way_below_elem q D HD). revert H. use factor_through_squash. { apply propproperty. } intros H. induction H as [ i H ]. refine (hinhpr (i ,, _)). exact (trans_dcpo p H). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics.