proposition: Lemma add_edge1n_diso (G : sgraph) (A : {set G}) (x y : G) : y \notin A -> diso (add_edges2 (add_edge G x y) [set x] A) (add_edges2 G [set x] (y |: A)).
proof: Proof. by move=> yNA; apply: eq_diso; exact: add_edge1n_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)