proposition: 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: 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.
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 UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Elements.Sharp