proposition: Theorem well_ordered_segment r s: worder r -> segmentp r s -> s = substrate r \/ (exists2 x, inc x (substrate r)& s = segment r x).
proof: Proof. move=> wor sr. case: (equal_or_not s (substrate r));[by left | move=> snr; right]. set y:= (substrate r) -s s. have ney: nonempty y by move: sr=> [sr _] ; apply: setC_ne. have tor := (worder_total wor); have or := proj1 tor. have sys: (sub y (substrate r)) by apply: sub_setC. move: (worder_prop wor sys ney)=> [x xy xle]. have xis: inc x (substrate r) by apply: sys. ex_tac;set_extens z => zs. apply/segmentP. have zsr: inc z (substrate r) by apply: (sub_segment1 sr). case: (total_order_pr2 tor zsr xis) => //. by case /setC_P: xy => [_ bad] /(proj2 sr _ _ zs). ex_middle zis. have zy: (inc z y) by apply/setC_P; split => // ;apply: (sub_segment zs). move: (xle _ zy) (inc_segment zs)=> p1 p2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)