fact: Definition ncp (U : {set G}) (p : G) : {set G} := locked [set x in CP U | connect (restrict [pred z:G | (z \in CP U) ==> (z == x)] sedge) p x].
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)