proposition: Lemma fconnect_switchE_aux u v : ~~ fconnect f x y -> fconnect (switch x y f) u v -> [|| fconnect f u v, fconnect f u x && fconnect f v y | fconnect f u y && fconnect f v x].
proof: Proof. move => n_xy. case: (boolP (fconnect f u v)) => //= fNuv sw_uv. have [Cu Cv] : u \in fclosure f (pred2 x y) /\ v \in fclosure f (pred2 x y). { have sw_inj := @switch_inj _ x y _ inj_f. have ? := fconnect_sym sw_inj. wlog suff S : u v fNuv sw_uv / u \in fclosure f (pred2 x y). by split; [exact: (S u v)|apply: (S v u)]; rewrite fconnect_sym. rewrite closure_switched // closure_pred2 // inE /= -!closure1 //. apply: contraNT fNuv; rewrite negb_or !inE ![_ _ _ u]fconnect_sym //. move/andP => [A B]. apply : sub_in_connect sw_uv => z Hz z' /=. rewrite /switch/= [z == x]rwF 1?[z == y]rwF //; by apply: contraTneq Hz => ->. } case/closureP : Cu => /= ? /pred2P [-> f_ux|-> f_uy]. case/closureP : Cv => /= ? /pred2P [-> f_vx|-> ->]; last by rewrite f_ux. apply: contraNT fNuv => _. apply: connect_trans f_ux _. by rewrite fconnect_sym. case/closureP : Cv => /= ? /pred2P [-> ->|-> f_vy]; first by rewrite f_uy. apply: contraNT fNuv => _. apply: connect_trans f_uy _. by rewrite fconnect_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)