proposition: Lemma del_node_adjn_face x : adjn z x -> exists d' : del_node , d' \in orbit face z' /\ cnode (val d') x.
proof: Proof. case/exists_inP => y; rewrite !inE => n_z_y n_x_ey. exists (Sub (face y) (wheel_proof n_z_y)); split. - rewrite -fconnect_orbit /z'; do 2 move: (wheel_proof _) => ?. by have:= neighbor_face_aux n_z_y; rewrite /inD !insubdT. - by rewrite /= cnode1 plain_eq' // cnodeC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)