Lemma strongly_maximal_apart {D : dcpo} (C : continuous_dcpo_struct D) {x y : D} (Hx : is_strongly_maximal x) (Hy : is_strongly_maximal y) (p : x # y) : is_hausdorff_separated x y. Proof. revert p. use factor_through_squash_hProp. intros [Hxy | Hyx]. - assert (Hb := continuous_not_specialization_weq C _ _ Hxy). revert Hb. use factor_through_squash_hProp. intros (b & Hbx & Hby). specialize (Hy b x Hbx). revert Hy. use factor_through_squash_hProp. intros [Hby' | Hxy' ]. + apply fromempty. use (Hby _). exact (way_below_to_le Hby'). + exact Hxy'. - assert (Hb := continuous_not_specialization_weq C _ _ Hyx). revert Hb. use factor_through_squash_hProp. intros (b & Hby & Hbx). specialize (Hx b y Hby). revert Hx. use factor_through_squash_hProp. intros [Hbx' | Hxy' ]. + apply fromempty. use (Hbx _). exact (way_below_to_le Hbx'). + apply symm_is_hausdorff_separated. exact Hxy'. 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. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Elements.Sharp.