proposition: Lemma merge_planar (G : hypermap) (x y : G) : ~~ gcomp x y || (cnode x y (+) cface x y) -> planar G -> planar (merge x y).
proof: Proof. by rewrite /planar => /genus_merge->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)