proposition: Lemma add_edge11_diso (G : sgraph) (x y : G) : diso (add_edge G x y) (add_edges2 G [set x] [set y]).
proof: Proof. apply: eq_diso; exact: add_edge11_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)