proposition: Lemma unique_lub : forall (f:nat->A)(x y: A), antisymmetric R -> lub x f -> lub y f -> x = y.
proof: Proof. intros f x y Ha Hx Hy. apply least_unique with (fun x => upper_bound x f); auto. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith