proposition: Lemma setI_segment r s: (alls s (segmentp r)) -> segmentp r (intersection s).
proof: Proof. move=> als; split; first by apply: setI_sub2 => x /als/proj1. move=> x y xi yx; case: (emptyset_dichot s) => nes. by move: xi; rewrite nes setI_0 => /in_set0. apply: (setI_i nes) => z zs; move: (als _ zs) => [_ p]. apply : p (setI_hi xi zs) yx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)