Lemma is_sharp_cotransitive_apartness_help {X : dcpo} (CX : continuous_dcpo_struct X) {x y z : X} (Hz : is_sharp z) (p : x ⊄ y) : x # z ∨ y # z. Proof. assert (H := continuous_not_specialization_weq CX x y p). revert H. use factor_through_squash. { apply propproperty. } intro u. induction u as [ u [ q₁ q₂ ]]. assert (H := unary_interpolation CX q₁). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ v [ r₁ r₂ ]]. assert (H := Hz u v r₁). revert H. use factor_through_squash. { apply propproperty. } intro s. induction s as [ s | s ]. - refine (hinhpr (inr (hinhpr (inr _)))). use (invmap (continuous_not_specialization_weq CX z y)). exact (hinhpr (u ,, s ,, q₂)). - refine (hinhpr (inl (hinhpr (inl _)))). use (invmap (continuous_not_specialization_weq CX x z)). exact (hinhpr (v ,, r₂ ,, s)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.