proposition: Lemma connected_bgraph (G : graph2) (U : {set G}) (x : G) : connected [set: skeleton G] -> x \in @CP (skeleton G) U -> connected [set: skeleton (bgraph U x)].
proof: Proof. move => conn_G cp_x. apply: connected_skeleton; rewrite imset_valT memKset //. exact: connected_bag. 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)