proposition: Lemma cnode_merge (G : hypermap) (x y u v : G) : ~~ cnode x y -> @cnode[merge G x y] u v = [|| @cnode[G] u v , @cnode[G] u x && @cnode[G] v y | @cnode[G] u y && @cnode[G] v x ].
proof: Proof. by apply: fconnect_switchE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)