fact: Record hiso := Hiso { hiso_dart :> bij G H; hiso_edge x : hiso_dart (edge x) = edge (hiso_dart x); hiso_node x : hiso_dart (node x) = node (hiso_dart x) }.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)