proposition: Lemma skip1 x : f x \in a -> skip x = f x.
proof: Proof. move => fx_a. case: (skipP' fx_a) => // n _ N1 N2. move: (N2 0 fx_a). by rewrite leqn0 => /eqP->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)