proposition: Lemma cpNI x y (p : Path x y) z : z \notin p -> z \notin cp x y.
proof: Proof. Proof using. case: (uncycle p) => p' S irr_p' av_z. apply/cpPn. exists p' => //. apply: contraNN av_z. exact: S. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)