proposition: Lemma edges_at_add_edge' G e x y z u : e \notin eset G -> x != z -> y != z -> edges_at (G ∔ [e,x,u,y]) z = edges_at G z.
proof: Proof. move => eGN xDz yDz. apply/fsetP => e0; rewrite !edges_atE /= !inE. case: (altP (e0 =P e)) => //= [->|e0De]. - by rewrite (negbTE eGN) /incident /= existsb_case !updateE (negbTE xDz) (negbTE yDz). - by rewrite /incident/= !existsb_case !update_neq. 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)