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 -> let x := source e in let y := target e in exists2 e, e \in E & (e \in edges x y) || (e \in edges y x)) -> @connected (skeleton (subgraph_for con)) U.
proof: Proof. move => U. set U' := val @: U => conn_U all_edges x y x_U y_U. case/connectP: (conn_U _ _ (imset_f val x_U) (imset_f val y_U)) => p. elim: p x x_U => [|a p IH] x x_U; first by move=> _ /val_inj <-; exact: connect0. rewrite (lock edge_rel) /= -!andbA -lock. case/and4P=> _ a_U' xa. have Ha : a \in V by case/imsetP: a_U' => b _ ->; exact: valP. set b : subgraph_for con := Sub a Ha. rewrite -[a]/(val b) => p_path p_last. have b_U : b \in U by rewrite -(mem_imset _ _ val_inj). apply: connect_trans (IH b b_U p_path p_last). apply: connect1 => /=. apply/andP; split; first by apply/andP; split. move: xa. rewrite -[a]/(val b). move: b x b_U x_U {p_last p_path a_U' IH p} => {a Ha} b x b_U x_U. rewrite /edge_rel/=/sk_rel -val_eqE. case/andP=> xNb. rewrite xNb /= => adjv_xb. wlog [e0] : b x b_U x_U xNb {adjv_xb} / exists e, e \in edges (val x) (val b). { move=> Hyp. case/existsP: adjv_xb => e. rewrite inE => /orP[]He. - by apply: Hyp => //; exists e. - rewrite adjacent_sym. apply: Hyp => //; by [rewrite eq_sym | exists e]. } rewrite inE. case/andP=> /eqP Hsrc /eqP Htgt. have Ne0 : source e0 != target e0 by rewrite Hsrc Htgt. have : e0 \in edge_set U' by rewrite inE Hsrc Htgt !imset_f. case/all_edges=> [//|] e' Ee'. rewrite Hsrc Htgt => He'. set e : edge (subgraph_for con) := Sub e' Ee'. have He : e \in edges x b :|: edges b x. { move: He'. by rewrite !inE -[e']/(val e) -!(inj_eq val_inj). } apply/existsP. by exists e. 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)