proposition: Lemma skip_exists x : x \in a -> [exists n : 'I_(order f (f x)), iter n.+1 f x \in a].
proof: Proof. move => x_a. apply: skip_exists' x_a _. by rewrite fconnect_sym // fconnect1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)