proposition: Lemma add_edge_remove_edgesK (G : pre_graph) e E x y u : e \in E -> G ∔ [e,x,u,y] - E ≡G (G - E).
proof: Proof. move => eE. have X : (e |` eset G) `\` E = eset G `\` E. { by rewrite fsetDUl fset1D eE fset0U. } split => //=; rewrite X. 1: move => b. all: move => f Hf; rewrite updateE //. all: apply: contraTneq Hf => ->; by rewrite inE eE. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)