proposition: Lemma skip_proof x : [exists n : 'I_(order f (f x)), iter n.+1 f x \in a] -> exists n : nat, iter n.+1 f x \in a.
proof: Proof. by case/existsP => n; exists n. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)