proposition: Lemma segmentc_insetof r x: worder r -> inc (segmentc r x) (segments r).
proof: Proof. move=> wo ; apply/(inc_segmentsP wo). apply: segmentc_segment; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)