fact: Definition i (z : G) : G' := Sub (Sub (Icp z) (S z)) SXe.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)