proposition: Lemma remove_vertex_add_edge (G : pre_graph) z x y u e : z != x -> z != y -> e \notin eset G -> add_edge' (G \ z) e x u y ≡G (add_edge' G e x u y) \ z.
proof: Proof. move => Hx Hy He. split => //=. rewrite edges_at_add_edge' ?[_ == z]eq_sym //. rewrite fsetDUl [[fset _] `\` _](fsetDidPl _ _ _) //. apply/fdisjointP => ? /fset1P ->. by rewrite edges_atE (negbTE He). 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)