Proposition discrete_eq_to_way_below {x y : discrete_dcpo X} (p : x = y) : x ≪ y. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.