proposition: Lemma supremum_pr2 r X a: order r -> least_upper_bound r X a -> a = supremum r X.
proof: Proof. move=> or le. have hs: has_supremum r X by exists a. exact: (supremum_unique or le (supremum_pr1 or hs)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)