proposition: Lemma del_node_plain : plain del_node.
proof: Proof. have pG := plainP plainG; apply/plainP => x _; split. - apply/val_inj => /=. rewrite !val_frestrict. by apply pG. - rewrite -(inj_eq val_inj) !val_frestrict. by apply pG. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)