proposition: Lemma inc_set_of_segments1 r x: order r -> inc x (segments r) -> segmentp r x.
proof: Proof. rewrite /segments/segmentss=> or. case /setU1_P. by move /funI_P => [z zr ->]; apply: segment_segment=>//. by move=> ->; apply: substrate_segment. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)