proposition: Lemma skip_eq x y n : x \in a -> y \in a -> (forall m : nat, iter m.+1 f x \in a -> n <= m) -> iter n.+1 f x = y -> skip x = y.
proof: Proof. move => x_a y_a min_n def_y; case: skipP => // m _ M1 M2. suff /eqP -> : m == n by []. by rewrite eqn_leq min_n // M2 // def_y. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)