proposition: Lemma remove_edges_connected (G : graph) (E : {set edge G}) : {in E, forall e : edge G, connect (@sk_rel _ _ (remove_edges E)) (source e) (target e)} -> connected [set: skeleton G] -> connected [set: skeleton (remove_edges E)].
proof: Proof. move=> E_conn G_conn. apply: connectedTI => x y. have := connectedTE G_conn x y. apply: connect_sub x y. move=> /=. apply skelP. - by move=> x y; rewrite connect_symI //; exact: sk_rel_sym (remove_edges E). - move=> e sNt. case: (boolP (e \in E)) => [/E_conn//|He]. apply: connect1. rewrite /edge_rel/=/sk_rel sNt /=. by apply/existsP; exists (Sub e He); rewrite !inE !eqxx. 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)