proposition: Lemma skipE x (x_a : x \in a) : skip x = iter (ex_minn (skip_proof (skip_exists x_a))).+1 f x.
proof: Proof. rewrite /skip. case: {-}_ / idP => [p|]; last by rewrite (skip_exists x_a). by rewrite (bool_irrelevance (skip_exists x_a) p). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)