proposition: Lemma segment_rp_p3 r s: order r -> (alls s (segment_rp r)) -> segment_rp r (intersection s).
proof: Proof. move => or al. case: (emptyset_dichot s) => nes. rewrite nes setI_0; apply: segment_r_p0. move:(nes) => [k ks]. split. move => t ti; exact: (proj1 (al _ ks) _ (setI_hi ti ks)). move => x y xI lxy; apply: (setI_i nes) => a ias. move: (al _ ias) => [_ sy]; exact :(sy _ _ (setI_hi xI ias) lxy). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)