proposition: Lemma remove_edges_cross (G : graph) (V : {set G}) (E : {set edge G}) (x y : G) : E \subset edge_set V -> sk_rel x y -> y \notin V -> @sk_rel _ _ (remove_edges E) x y.
proof: Proof. move=> E_subV xy yNV. have {yNV} : (x \notin V) || (y \notin V) by rewrite yNV. pattern x, y. revert x y xy. apply skelP ; first by move=> x y; rewrite orbC sk_rel_sym. move=> e sNt stNV. rewrite /sk_rel sNt /=. case: (boolP (e \in E)) => He; last first. - apply/existsP; exists (Sub e He); by rewrite !inE !eqxx. - move: He stNV => /(subsetP E_subV). rewrite inE. by case/andP=> -> ->. 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)