proposition: Lemma inc_segmentsP r: worder r -> forall x, (segmentp r x <-> inc x (segments r)).
proof: Proof. move => wor x; split=> hyp. case: (well_ordered_segment wor hyp). by move => ->; apply /setU1_P; right. move=> [y ysr ->]; apply /setU1_P; left; apply/funI_P; ex_tac. move:wor=> [or wor]. case /setU1_P: hyp. by move/funI_P => [z zr ->]; apply: segment_segment. by move=> ->; apply: substrate_segment. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)