proposition: Lemma del_node_loopless : loopless del_node.
proof: Proof. Proof using llG. move/existsPn : (llG) => llG'; apply/existsPn => x. apply: contraNN (llG' (val x)) => loop_x. suff S (u v : del_node) : cnode u v -> cnode (val u) (val v). { by rewrite -[X in cnode _ X](val_frestrict del_edge_hom) S. } rewrite /= -(@fconnect_skip _ [predC N] _ nodeI); try exact: valP. by apply: homo_connect => {u v} u v /= /eqP<-; rewrite val_frestrict. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)