proposition: Lemma sinterval_noedge_cp (x y z u v : G) : u -- v -> u \in sinterval x z -> v \in sinterval z y -> z \notin cp x y.
proof: Proof. Proof using. move=> uv /sintervalP2[][p _ /negbTE zNp] _ /sintervalP2[_][q _ /negbTE zNq]. apply/cpP => /(_ (pcat (prev p) (pcat (edgep uv) q))). rewrite !mem_pcat mem_prev mem_edgep zNp zNq orbF /=. apply/negP. rewrite negb_or. apply/andP. split. - apply: contraFneq zNp =>->. exact: path_begin. - apply: contraFneq zNq =>->. exact: path_begin. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)