proposition: Lemma bag_cp (U : {set G}) x y : x \in CP U -> y \in CP U -> x \in bag U y = (x == y).
proof: Proof. Proof using G_conn. move => cp_x cp_y. apply/idP/idP => [|/eqP <-]; last exact: bag_id. apply: contraTT => xy. have D: [disjoint bag U x & bag U y] by apply : bag_disj. by rewrite (disjointFr D) // bag_id. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)