proposition: Lemma connected_skeleton (G : graph) V E (con : @consistent _ _ G V E) : forall U : {set subgraph_for con}, @connected (skeleton G) (val @: U) -> (forall e, e \in edge_set (val @: U) -> source e != target e -> e \in E) -> @connected (skeleton (subgraph_for con)) U.
proof: Proof. move=> U conn_U all_edges. apply: connected_skeleton' conn_U _. move=> e E1 E2; exists e; rewrite ?inE ?eqxx //. exact: all_edges. 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)