proposition: Lemma cpP x y z : reflect (forall p : Path x y, z \in p) (z \in cp x y).
proof: Proof. Proof using. apply: introP. - move => cp_z p. apply: contraTT cp_z. exact: cpNI. - case/cpPn => p _ av_z /(_ p). exact/negP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)