proposition: Lemma cantor_worder r (ssub := fun E => Zo (substrate r)(fun z => forall x, inc x E -> glt r x z)): order r -> nonempty (substrate r) -> ( worder r <-> ( (has_least r) /\ (forall F, sub F (substrate r) -> nonempty F -> nonempty (ssub F) -> (has_least (induced_order r (ssub F)))))).
proof: Proof. move => or nesr; split. move => [_ wor ]; split;first by apply: worder_least. move => F sfr nef nef1; apply: wor => //; apply: Zo_S. move => [[y [ysr ly]] pb]; split => //. move => x xsr [x0 x0x]. case: (inc_or_not y x). move => yx; exists y; red; rewrite (iorder_sr or xsr); split => //. by move => t tx; apply /iorder_gle0P => //; apply: ly; apply: xsr. move => nyx. set F:= Zo (substrate r) (fun z => forall t, inc t x -> glt r z t). have sf1: sub F (substrate r) by apply: Zo_S. have yf1: inc y F. apply: Zo_i => // t tx; split; [ apply: (ly _ (xsr _ tx)) | dneg yt; ue]. set G := ssub F. have pa : sub x G. move => t tx; apply: Zo_i; first by apply: xsr. by move => tv /Zo_P [_ aux]; apply: aux. have neG: nonempty G by exists x0; apply: pa. have neF: nonempty F by exists y. have sg: sub (ssub F) (substrate r) by apply: Zo_S. move: (pb _ sf1 neF neG) => [a []]; rewrite (iorder_sr or sg) => aG h. exists a; hnf; rewrite (iorder_sr or xsr). have qa: forall t, inc t x -> gle r a t. move => t tx. move: (h _ (pa _ tx)) => cp1; exact (iorder_gle1 cp1). case: (inc_or_not a x) => iax. by split => // t tx; apply /iorder_gle0P => //; apply: qa. have aF: inc a F. apply: Zo_i; [by apply: sg | move => t tx; split;[ by apply: qa| dneg ta;ue]]. by move: aG => /Zo_P [_ p]; move: (p _ aF) => [_]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)