proposition: Lemma hiso_face (i : hiso) x : i (face x) = face (i x).
proof: Proof. by rewrite -{2}[x]faceK hiso_edge hiso_node nodeK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)