proposition: Lemma lubP r X: order r -> sub X (substrate r) -> forall x, (least_upper_bound r X x <-> (upper_bound r X x /\ forall z, upper_bound r X z -> gle r x z)).
proof: Proof. rewrite /least_upper_bound/least_induced/least=>or Xr x. set T:= Zo _ _. have sT: sub T (substrate r) by apply: Zo_S. rewrite (proj2 (iorder_osr or sT)). have tp z : inc z T <-> upper_bound r X z. by split; [ case/Zo_P | move => lb;apply:Zo_i => //; case:lb]. split. move=> [/tp ha hyp]; split => // z lbz. move/tp: lbz => /hyp;apply: iorder_gle1. move=> [lbx hyp]; move/tp: (lbx) => xT. by split => // y yT; apply /iorder_gle0P=> //; apply:hyp; apply/tp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)