proposition: 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: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness UniMath.OrderTheory.DCPOs.Basis.Continuous