Proposition is_sharp_cotransitive_apartness {X : dcpo} (CX : continuous_dcpo_struct X) {x y z : X} (Hz : is_sharp z) (p : x # y) : x # z ∨ y # z. Proof. revert p. use factor_through_squash. { apply propproperty. } intro p. induction p as [ p | p ]. - exact (is_sharp_cotransitive_apartness_help CX Hz p). - assert (H := is_sharp_cotransitive_apartness_help CX Hz p). revert H. use factor_through_squash. { apply propproperty. } intro q. induction q as [ q | q ]. + exact (hinhpr (inr q)). + exact (hinhpr (inl q)). 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.