proposition: Proposition eq_lub {x y : X} (Hx : is_least_upperbound x) (Hy : is_least_upperbound y) : x = y.
proof: Proof. pose (x' := (x ,, Hx) : lub). pose (y' := (y ,, Hy) : lub). use (antisymm_PartialOrder PX). - apply (lub_is_least x' y'). exact (lub_is_upperbound y'). - apply (lub_is_least y' x'). exact (lub_is_upperbound x'). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets