proposition: Lemma supremum_pr1 X r: order r -> has_supremum r X -> least_upper_bound r X (supremum r X).
proof: Proof. move => or [z h]. apply: the_least_pr => //; last by exists z. exact: (proj1 (iorder_osr or (Zo_S(p:=upper_bound r X)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)