proposition: Lemma edges_at_add_edge (G : pre_graph) x y e u : edges_at (G ∔ [e, x, u, y]) y = e |` edges_at G y.
proof: Proof. apply/fsetP => e0. rewrite inE !edges_atE /= !inE. case: (altP (e0 =P e)) => //= [->|e0De]. - rewrite /incident/=. existsb true. by rewrite !update_eq. - rewrite /incident/=. by rewrite !existsb_case !updateE. 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)