proposition: Lemma ncp_CP (U : {set G}) (u : G) : u \in CP U -> ncp U u = [set u].
proof: Proof. Proof using. move => Hu. apply/setP => x. rewrite [_ \in [set _]]inE. apply/ncpP/eqP. - move => [Hx [q Hq]]. by rewrite [u]Hq. - move => ->. split => //. exists (idp u) => y _. by rewrite mem_idp => /eqP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)