proposition: Lemma neighbor_face_aux x : cnode z x -> cface (inD (face z)) (inD (face x)).
proof: Proof. case/connectP => p pth_p ->; elim/last_ind: p pth_p => // p y IH. rewrite last_rcons rcons_path => /andP[A /eqP <-]. by apply: connect_trans (IH A) _; apply: wheel_segment; apply/connectP; exists p. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)