proposition: Lemma add_node_diso (G : sgraph) (A : {set G}) (x : G) : x \in A -> diso (add_edges2 (add_node G [set x]) [set None] (Some @: (A :\ x))) (add_node G A).
proof: Proof. by move=> x_A; exact/eq_diso/add_node_diso_proof. Defined.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)