Proposition antisymm_way_below {x y : X} (p : x ≪ y) (q : y ≪ x) : x = y. Proof. use antisymm_dcpo. - apply way_below_to_le. exact p. - apply way_below_to_le. exact q. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics.