proposition: Lemma sinterval_exit x y u v : u \notin sinterval x y -> v \in sinterval x y -> x \in cp u v \/ y \in cp u v.
proof: Proof. Proof using. rewrite !inE negb_and !negbK => H. wlog: x y {H} / x \in cp u y. { move => W. case/orP : H; first exact: W. rewrite andbC => A B. move: (W _ _ A B). tauto. } move => Hu /andP[Hv1 Hv2]. left. apply: contraTT Hu => C. exact: cpN_trans Hv1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)