proposition: Lemma adjn_loopless (D : hypermap) (x y : D) : loopless D -> cnode x y -> adjn x y = false.
proof: Proof. move => llD n_xy. apply: contraNF llD => /exists_inP[z]; rewrite !inE => n_xz n_y_ez. existsb z. apply: connect_trans n_y_ez. apply: connect_trans n_xy. by rewrite cnodeC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)