proposition: Lemma bag_disj (U : {set G}) x y : x \in CP U -> y \in CP U -> x != y -> [disjoint bag U x & bag U y].
proof: Proof. Proof using G_conn. move => Ux Uy xy. apply/pred0P => p /=. apply:contraNF xy => /andP[]. rewrite !ncp_bag //. by move => /eqP-> /eqP/set1_inj->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)