proposition: Lemma edgeless_bag (G : graph) (U : {set G}) (x : skeleton G) : connected [set: skeleton G] -> x \in @CP G U -> edge_set (@bag G U x) == set0 -> @bag G U x == [set x].
proof: Proof. move => con_G cp_x. apply: contraTT => /bag_nontrivial [y Y1 Y2]. rewrite eq_sym in Y2. have con_Px := connected_bag con_G cp_x. have [||z Pz xz] := connected_card_gt1 con_Px _ _ Y2. exact: bag_id. done. apply/set0Pn. apply: get_edge xz => //. exact: bag_id. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)