proposition: Lemma iter_inj n : injective (iter n f).
proof: Proof. move => x y. by elim: n => // n IH /= /inj_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)