proposition: Lemma add_edge11_diso_proof (G : sgraph) (x y : G) : add_edge_rel x y =2 add_edges2_rel _ [set x] [set y].
proof: Proof. move => u v; rewrite /= !in_set1 andb_orr; congr [|| _ , _ | _]. by rewrite [v == u]eq_sym [(v == x) && _]andbC. Qed.
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)