proposition: Lemma del_node_adjn (u v : del_node) : adjn u v = adjn (val u) (val v).
proof: Proof. Proof using plainG. apply/exists_inP/exists_inP => -[d]; rewrite !inE. by rewrite !del_node_cnode val_frestrict; exists (val d). have [dN|dNN] := boolP (d \in N); last first. by exists (Sub d dNN); rewrite inE del_node_cnode ?val_frestrict. move => n_u_d n_v_d; case:notF. have/NP/orP[n_z_d|n_z_ed] := dN. - apply: contraNT (valP u) => _. apply: mem_closure. by rewrite inE (connect_trans n_z_d _) // cnodeC. - apply: contraNT (valP v) => _. apply: mem_closure. by rewrite inE (connect_trans n_z_ed _) // cnodeC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)