proposition: Lemma cpxx x : cp x x = [set x].
proof: Proof. Proof using. apply/eqP. rewrite eqEsubset sub1set mem_cpl andbT. apply/subsetP => z /cpP /(_ (idp x)). by rewrite !inE mem_idp. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)