proposition: Lemma supremum_unique X r: order r -> uniqueness (least_upper_bound r X).
proof: Proof. rewrite /least_upper_bound => or. exact:(unique_least (proj1 (iorder_osr or (Zo_S (p:=upper_bound r X))))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)