proposition: Lemma add_vertexK (G : pre_graph) (isG : is_graph G) x a : x \notin vset G -> G ∔ [x, a] \ x ≡G G.
proof: Proof. move => Hx. split => //=. - by rewrite fsetU1K. - by rewrite edges_at_added_vertex // fsetD0. - rewrite fsetU1K // => y Hy. rewrite update_neq //. by apply: contraNneq Hx => <-. 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)