proposition: Lemma fconnect_switched (xDy : x != y) : fconnect xswitch x y = ~~ fconnect f x y.
proof: Proof. have ? := switch_inj. apply/idP/idP. - apply: contraTN => fc_xy; rewrite same_fconnect1 //= eqxx. have [? ?] : fconnect f (f y) y /\ fconnect f (f y) x. { by rewrite -!same_fconnect1 ?connect0 1?fconnect_sym. } pose m := findex f (f y) x; pose n := findex f (f y) y. have m_lt_n : m < n. { rewrite /m /n ltn_neqAle; apply/andP; split. - apply: contra_neq (xDy). by apply: index_inj; rewrite -fconnect_orbit. - by rewrite -{3}[y](finv_f inj_f) findex_finv -ltnS orderSpred findex_max. } have switch_f k : k <= m -> iter k xswitch (f y) = iter k f (f y). { apply: iter_switchE => j j_lt_k. rewrite !inE negb_or. rewrite !before_findex -?same_fconnect1 -1?fconnect_sym //. exact: ltn_trans j_lt_k _. } have: looping xswitch (f y) m.+1. { by rewrite /looping trajectS iterS switch_f // iter_findex /= ?eqxx ?mem_head. } apply: iter_looping => k k_lt_m. rewrite switch_f //. apply: before_findex => //. exact: leq_trans m_lt_n. - move => N. rewrite same_fconnect1 //= eqxx. apply: fconnect_f_switch. + by rewrite -same_fconnect1_r. + by rewrite -same_fconnect1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)