proposition: Lemma segmentc_segment r x: order r -> segmentp r (segmentc r x).
proof: Proof. move=> or; split; first by apply: Zo_S. move=> a b /Zo_P [asr ax] ba; apply: Zo_i; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)