proposition: Lemma iter_switchE z m : (forall n, n < m -> iter n f z \in [predC pred2 x y]) -> forall k, k <= m -> iter k xswitch z = iter k f z.
proof: Proof. move => H k lt_m. have {H lt_m m} : forall n : nat, n < k -> iter n f z \in [predC pred2 x y]. { by move => n Hn; apply: H; apply: leq_trans lt_m. } elim: k z => // k IH z Hk; rewrite !iterSr switchE ?IH // ; last exact: (Hk 0). move => n Hn; by rewrite -iterSr Hk // ltnS. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)