proposition: Lemma ncp0 (U : {set G}) x p : x \in CP U -> ncp U p == set0 = false.
proof: Proof. Proof using G_conn. case/connect_irredP : (G_conn p x) => q irr_q Ux. case: (split_at_first Ux (path_end q)) => y [q1] [q2] [def_q CPy Hy]. suff: y \in ncp U p. { apply: contraTF => /eqP->. by rewrite inE. } apply/ncpP. split => //. by exists q1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)