fact: Definition add_vlabel (G: graph) (x: G) (a: Lv): graph := @Graph (vertex G) (edge G) (@endpoint _ _ G) (fun v => if v==x then a ⊗ vlabel v else vlabel v) (@elabel _ _ G).
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)