proposition: Lemma mergeC_hiso (G : hypermap) (x y : G) : hiso (merge G x y) (merge G y x).
proof: Proof. hiso bij_id => // z; exact: (@switchC G x y (@node G) z). Defined.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)