proposition: Lemma connected_CP_closed (U V : {set G}) : connected V -> U \subset V -> CP U \subset V.
proof: Proof. Proof using. move=> V_conn /subsetP UV. apply/bigcupsP. case=> x y /=. rewrite in_setX. case/andP=> /UV Hx /UV Hy. apply: connected_cp_closed => //. by rewrite subUset !sub1set. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)