proposition: Lemma Exercise1_11b r: order r -> (forall X, sub X (substrate r) -> has_supremum r X) -> complete_lattice r.
proof: Proof. move=> or h; split => //. move=> X Xsr;split;fprops. set (Z := (Zo (substrate r) (lower_bound r X))). have zs: (sub Z (substrate r)) by apply: Zo_S. move: (h _ zs) => [x] /(lubP or zs) [[xz ux] leux]. exists x;apply /(glbP or Xsr); split. split; first exact. move=> y yX; apply: leux; split; first by apply: Xsr. by move=> t /Zo_P [_ [_]]; apply. by move => z zl; apply: ux; apply: Zo_i => //;move: zl =>[ok _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)