proposition: Lemma ncp_interval U (x y p : G) : x != y -> [set x; y] \subset ncp U p -> p \in sinterval x y.
proof: Proof. Proof using. rewrite subUset !sub1set inE => xy /andP[Nx Ny]. wlog suff: x y xy Nx Ny / x \notin cp p y. { move => W. by rewrite !W // eq_sym. } have cp_x : x \in CP U. by case/ncpP : Nx. case/ncpP : Ny => cp_y [q /(_ _ cp_x) H]. apply: (cpNI (p := q)). by apply: contraNN xy => /H->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)