proposition: Lemma bag_edges_disj (G : graph) (U : {set G}) (x y : G) : connected [set: skeleton G] -> x \in @CP G U -> y \in @CP G U -> x != y -> [disjoint edge_set (@bag G U x) & edge_set (@bag G U y)].
proof: Proof. move=> G_conn x_cp y_cp xNy. rewrite -setI_eq0 -subset0. apply/subsetP => e. rewrite 3!inE. case/andP=> /andP[src_x tgt_x] /andP[src_y tgt_y]. by case: (disjointE (@bag_disj G _ U x y _ _ _) src_x src_y). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)