proposition: Proposition trans_way_below {x y z : X} (p : x ≪ y) (q : y ≪ z) : x ≪ z.
proof: 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 ]. assert (H' : y ⊑ ⨆ D). { refine (trans_dcpo H _). use (less_than_dcpo_lub D _ i). apply refl_dcpo. } exact (way_below_elem p D H'). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics