proposition: Lemma Exercise6_9 r: worder r -> (forall x, inc x (substrate r) -> (least r x \/ has_greatest (induced_order r (segment r x)))) -> r \Is Nat_order \/ (exists2 n, natp n & r \Is (Nint_co n)).
proof: Proof. move => wor hyp. move: Nat_order_wor => [h1 s1]. case: (isomorphism_worder2 wor h1);first (by left); last first. move=> [n]; rewrite s1;move => nN io1; right => //; exists n => //. by rewrite (Exercise6_9a nN);apply: orderIS. move=> [x xsr [f [o1 o2 [bf sf tg] etc]]]. have pa: sub (segment r x) (substrate r) by apply: sub_segment. move: wor => [or _];move: sf; aw => sf. have sra := (proj2(seg_order_osr x or)). rewrite s1 in tg. case: (hyp _ xsr) => aux. have zt: inc \0c (target f) by rewrite tg ; apply: NS0. move: (inverse_Vis bf zt); rewrite sf sra => ys. move: (inc_segment ys) => ylt. move: aux => [a1 a2]; move: (a2 _ (sub_segment ys)) => yle; order_tac. move: aux => [y]; rewrite /greatest iorder_sr //; move => [ysr yfg]. rewrite - sra - sf in ysr. have wb:(natp (Vf f y)) by rewrite/natp; Wtac; fct_tac. set z := csucc (Vf f y). have zb: inc z (target f) by rewrite tg; apply/NS_succ. have ys:= (inverse_Vis bf zb); move:(ys) ;rewrite sf sra => ys1. move: (yfg _ ys1); rewrite (etc _ _ ys ysr). rewrite (inverse_V bf zb) /z. move /Nat_order_leP => [qa qb qc]. case: (cleNgt qc (cltS qb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)