proposition: Lemma remove_edges_restrict (G : graph) (V : {set G}) (E : {set edge G}) (x y : G) : E \subset edge_set V -> connect (restrict (~: V) (@sk_rel _ _ G)) x y -> connect (@sk_rel _ _ (remove_edges E)) x y.
proof: Proof. move=> E_subV. apply: connect_mono x y => x y /=. rewrite !inE -andbA. case/and3P=> xNV yNV xy. exact: remove_edges_cross xy yNV. 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)