proposition: Lemma merge_loopless (D : hypermap) (x y : D) : plain D -> ~~ @cnode[D] x y -> ~~ @adjn[D] x y -> loopless D -> loopless (merge D x y).
proof: Proof. move => plainD nNxy nAxy ; apply: contraNN => /existsP [z]. rewrite cnode_merge // => /or3P[?|/andP[Z1 Z2]|/andP[Z1 Z2]]; first by apply/existsP; exists z. apply: contraNT nAxy => _. by apply: (adjnI D z); rewrite cnodeC. apply: contraNT nAxy => _. by apply: (adjnI D (edge z)); rewrite cnodeC ?plain_eq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)