proposition: Theorem segments_worder r: worder r -> worder (sub_order (segments r)).
proof: Proof. move=> wor; move: (wor)=> [or _];move: (worder_total wor)=> tor. have [oi sr] := (sub_osr (segments r)). apply:(worder_prop_rev oi); rewrite sr => x xsr nex. set y := x \cap (segmentss r). case: (emptyset_dichot y) => hy. have xv: x = singleton (substrate r). apply: set1_pr1=>// z zx. case /setU1_P: (xsr _ zx) => //. by move=> aux; empty_tac1 z; apply: setI2_i. have srx: inc (substrate r) x by rewrite xv; fprops. by ex_tac; rewrite xv; move=> z /set1_P ->; order_tac;rewrite sr; apply:xsr. have ysr: sub y (segmentss r) by move => t ty; apply: (setI2_2 ty). have segp a: inc a y -> exists2 u, inc u (substrate r) & a = segment r u. by move=> /ysr /funI_P. pose cf a := select(fun u => a = segment r u) (substrate r). have cfp: forall a, inc a y -> (inc (cf a) (substrate r) /\ a = segment r (cf a)). move=> a ay; move: (segp _ ay) => [u us uv]. have <- //: u = cf a. apply: (select_uniq _ us uv); move => c b csr sc bsr sb. by apply: (segment_injective (worder_total wor) csr bsr); rewrite - sb - sc. set (z:= fun_image y cf). have nez: nonempty z by apply: funI_setne. have zsr: sub z (substrate r). by move => t /funI_P [u uy ->]; move: (cfp _ uy)=> [res _]. move: (worder_prop wor zsr nez) => [a asr lea]. have sax: (inc (segment r a) x). move: asr => /funI_P [u uy ->]. move: (cfp _ uy)=> [h <-]; apply: (setI2_1 uy). ex_tac;move=> b bx; apply/sub_gleP; split; fprops. case /setU1_P: (xsr _ bx); [ move => h | by move=>->; apply: sub_segment ]. have biy: (inc b y) by apply: setI2_i. have cbz: (inc (cf b) z) by apply /funI_P; ex_tac. move: (lea _ cbz). by move: (cfp _ biy)=> [p1 {2} ->]; apply: segment_monotone. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)