proposition: Lemma worder_numerable r: worder r -> numerable r.
proof: Proof. move=> wor; apply: segments_numerables =>// x xsr. set r' := fun x => induced_order r (segment r x). set (A:= Zo (substrate r)(fun z=> ~numerable (r' z))). case: (p_or_not_p (numerable (induced_order r (segment r x)))) =>// h. have sA: (sub A (substrate r)) by apply: Zo_S. have neA: nonempty A by exists x; apply/Zo_P. move: (wor)=> [or aux]; move: (aux _ sA neA)=> [y []]; rewrite iorder_sr// => ys yp. have rec: forall z, glt r z y -> numerable (r' z). move=>z zy; case: (p_or_not_p (numerable (r' z))) =>// nnz. have zA: (inc z A) by rewrite /A; apply: Zo_i=>//; order_tac. move: (iorder_gle1 (yp _ zA)) => yz; order_tac. move: ys => /Zo_P [ys ny]; case: ny. have sss: sub (segment r y) (substrate r) by apply: sub_segment. apply: segments_numerables; first by apply: induced_wor. rewrite /r' iorder_sr//; move=> z zy. have rzy: glt r z y by apply /segmentP. rewrite segment_induced // iorder_trans //;first by apply: rec. apply: segment_monotone =>//; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)