proposition: Proposition discrete_eq_to_way_below {x y : discrete_dcpo X} (p : x = y) : x ≪ y.
proof: Proof. induction p. intros D HD. assert (H := directed_set_el D). revert H. use factor_through_squash. { apply propproperty. } intros i. refine (hinhpr (i ,, _)). rewrite (less_than_dcpo_lub D (D i) i (refl_dcpo _)). exact HD. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous