proposition: Lemma segment_dichot_sub r x y: worder r -> segmentp r x -> segmentp r y -> (sub x y \/ sub y x).
proof: Proof. move=> wo sx sy. case: (well_ordered_segment wo sx). by move=> ->; right; apply: sub_segment1. case: (well_ordered_segment wo sy). by move=> ->; left; apply: sub_segment1. move=>[b br ->] [a ar ->]. by case: (proj2 (worder_total wo) _ _ ar br) => le; [left | right]; apply: (segment_monotone (proj1 wo)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)