proposition: Lemma cpTI x y z : (forall p : Path x y, irred p -> z \in p) -> z \in cp x y.
proof: Proof. Proof using. move => H. by apply/cpPn => [[p] /H ->]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)