proposition: Lemma switch_disconnected_lr u v : ~~ fconnect f x y -> fconnect f x u -> fconnect f y v -> fconnect (switch x y f) u v.
proof: Proof. case: (eqVneq x y) => [->|xDy]; first by rewrite connect0. move => xy. move: (xy); rewrite -fconnect_switched // => sxy xu yv. apply: connect_trans _ (switch_subrel xy yv). apply: connect_trans sxy. apply: (switch_subrel xy). by rewrite fconnect_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)