proposition: Lemma switch_subrel x y : ~~ fconnect f x y -> subrel (fconnect f) (fconnect (switch x y f)).
proof: Proof. move => n_xy u v. case/connectP => p; elim: p u => [|z p IHp] u /=; first by move => _ ->. move => /andP[/eqP fu pth_p] lst_p. apply: (connect_trans (y := z)); last exact: IHp. rewrite -fu => {IHp z pth_p lst_p fu}. have [u_xy|uNxy] := boolP (u \in pred2 x y); last first. by apply: connect1; rewrite [switch]lock /= -lock switchE. case/pred2P : u_xy => ->; first exact: fconnect_switch_x_fx. by rewrite fswitchC; apply: fconnect_switch_x_fx; rewrite fconnect_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)