proposition: Lemma CP_mono (U U' : {set G}) : U \subset U' -> CP U \subset CP U'.
proof: Proof. Proof using. move/subsetP => A. apply/bigcupsP => [[x y] /setXP [/A Hx /A Hy] /=]. apply/subsetP => z Hz. apply/bigcupP; exists (x,y) => //. exact/setXP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)