proposition: Lemma skip_first x y : y \in a -> fconnect f (f x) y -> f x \notin a -> skip x = skip (f x).
proof: Proof. move => y_a f_xy fxNa. have f_xy' : fconnect f (f (f x)) y. { move/iter_findex : f_xy. case: (findex _ _ _) => [/= dy|n]. by rewrite dy y_a in fxNa. rewrite iterSr => <-. exact: fconnect_iter. } case: (skipP' y_a f_xy) => n N0 N1 N2. case: (skipP' y_a f_xy') => m M0 M1 M2. suff /eqP-> : n == m.+1 by rewrite iterSr. rewrite eqn_leq N2 1?iterSr //=. destruct n as [|n]; first by rewrite /= (negbTE fxNa) in N1. by rewrite ltnS M2 // -iterSr. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)