proposition: Lemma fconnect_switchE 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. apply/idP/idP; first exact: fconnect_switchE_aux. case/or3P; first exact: switch_subrel. by case/andP => ? ?; apply: switch_disconnected_lr => //; by rewrite fconnect_sym. case/andP => ? ?. rewrite fconnect_sym; last exact: switch_inj. apply: switch_disconnected_lr => //; by rewrite fconnect_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)