proposition: Lemma del_node_neighbor1 x : ~~cnode z x -> x \in N -> node x \notin N.
proof: Proof. move=> /negPf n_zxF /NP; rewrite n_zxF /= => n_z_ex. apply: contraTN isT => /NP; rewrite -cnode1r n_zxF /= => n_z_enx. have /negbT := deg2 x; rewrite -(inj_eq edgeI) => /simple. by rewrite !plain_eq // (connect_trans _ n_z_ex) cnodeC // -cnode1r connect0 => /(_ isT). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)