proposition: Lemma segment_segment r x: order r -> segmentp r (segment 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)