proposition: Lemma worder_hassup r A: worder r -> sub A (substrate r) -> bounded_above r A -> has_supremum r A.
proof: Proof. move=> H As [t tA]. rewrite /has_supremum /least_upper_bound. set X:= (Zo _ _). have Xs: sub X (substrate r) by apply: Zo_S. have nX: (nonempty X) by exists t; apply: (Zo_i (proj1 tA) tA). by move: ((proj2 H) _ Xs nX)=> [x leX]; exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)