proposition: Lemma CP_set2 (x y : G) : CP [set x; y] = cp x y.
proof: Proof. Proof using. apply/setP => z. apply/bigcupP/idP => /=. + case=> -[a b] /=/setXP[]. rewrite !inE =>/orP[]/eqP->; last rewrite (cp_sym x y); move=>/orP[]/eqP->//; rewrite cpxx inE => /eqP->; by rewrite mem_cpl. + move=> Hz. exists (x, y) => //. by apply/setXP; rewrite !inE !eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)