proposition: Lemma ncpP (U : {set G}) (p : G) x : reflect (x \in CP U /\ exists q : Path p x, forall y, y \in CP U -> y \in q -> y = x) (x \in ncp U p).
proof: Proof. Proof using. rewrite /ncp -lock inE. apply: (iffP andP) => [[cp_x A]|[cp_x [q Hq]]]; split => //. - case: (boolP (p == x)) => [/eqP ?|px]. + subst p. exists (idp x) => y _ . by rewrite mem_idp => /eqP. + case/(connect_irredRP px) : A => q irr_q /subsetP sub_q. exists q => y CPy /sub_q. by rewrite !inE CPy => /eqP. - apply: (connectRI q) => y y_in_q. rewrite inE. apply/implyP => A. by rewrite [y]Hq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)