fact: Variables (T : Type) (P : pred T) (f : T -> T) (hom_f : {homo f : x / x \in P}).
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)