proposition: Lemma cp_triangle z {x y} : cp x y \subset cp x z :|: cp z y.
proof: Proof. Proof using. apply/subsetP => u /cpP => A. apply: contraT. rewrite !inE negb_or => /andP[/cpPn [p1 _ up1]] /cpPn [p2 _ up2]. move: (A (pcat p1 p2)). by rewrite mem_pcat (negbTE up1) (negbTE up2). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)