Proposition is_sharp_tight_apartness {X : dcpo} (CX : continuous_dcpo_struct X) {x y : X} (Hx : is_sharp x) (Hy : is_sharp y) (p : ¬(x # y)) : x = y. Proof. use antisymm_dcpo. - use (is_sharp_to_le CX Hy). intro q. apply p. exact (hinhpr (inl q)). - use (is_sharp_to_le CX Hx). intro q. apply p. exact (hinhpr (inr 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.