proposition: Lemma sinterval_disj_cp (x y z : G) : z \in cp x y -> [disjoint sinterval x z & sinterval z y].
proof: Proof. Proof using. move=> z_cpxy. rewrite -setI_eq0 -subset0. apply/subsetP=> u. rewrite inE. case/andP=> /sintervalP2[][p _ /negbTE zNp] _ /sintervalP2[_][q _ /negbTE zNq]. rewrite !inE. apply: contraTT z_cpxy => _. apply/cpP => /(_ (pcat (prev p) q)). by rewrite mem_pcat mem_prev zNp zNq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)