proposition: Proposition trans_le_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 ]. refine (hinhpr (i ,, _)). exact (trans_dcpo p H). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics