proposition: Lemma worder_has_empty_seg r: worder r -> nonempty (substrate r) -> exists2 x, inc x (substrate r) & segment r x = emptyset.
proof: Proof. move=> wor nes. move:(worder_least wor nes) =>[x [xsr xle]]; ex_tac. apply /set0_P => y /segmentP ys. have ysr: inc y (substrate r) by order_tac. move: (xle _ ysr) (proj1 wor) => le1 or; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)