proposition: Lemma skip_inj : {in a&, injective skip}.
proof: Proof. move => x y x_a y_a. case: (skipP x_a) => n _ N1 N2. case: (skipP y_a) => m _ M1 M2 eqI. suff/eqP ? : n == m by subst; apply: iter_inj eqI. case: (ltngtP n m) => // n_lt_m. - have eq_x : x = iter (m - n.+1).+1 f y. { rewrite subnSK //. rewrite -(subnK (ltnW n_lt_m)) -addnS addnC iterD in eqI. exact: iter_inj eqI. } rewrite eq_x in x_a. move: (M2 _ x_a). destruct m => //. by rewrite subSS ltn_subrR. - have eq_y : y = iter (n - m.+1).+1 f x. { rewrite subnSK //. rewrite -(subnK (ltnW n_lt_m)) -addnS addnC iterD in eqI. symmetry. exact: iter_inj eqI. } rewrite eq_y in y_a. move: (N2 _ y_a). destruct n => //. by rewrite subSS ltn_subrR. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)