proposition: Lemma segment_alt1 r s: worder r -> segmentp r s -> s = substrate r \/ (exists x, exists a, s = interval_co r a x).
proof: Proof. move => wo iss. case: (emptyset_dichot (substrate r)) => sre. by left; move: iss=> []; rewrite sre => /sub_set0. case: (well_ordered_segment wo iss); first by left. move: (worder_least wo sre) => [a lea] [x xsr p]. by right; exists x, a; rewrite - segment_alt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)