proposition: Lemma fconnect_f_switch z : ~~ fconnect f x z -> fconnect f z y -> fconnect xswitch z y.
proof: Proof. move => N /connectP [p]; elim: p z N => //= [_ _ _ -> //|u p IH z N /andP[/eqP E P L]]. have zDx : z != x by apply: contraNneq N => ->. case: (altP (z =P y)) => [-> //|zDy]. apply: connect_trans (connect1 _) (IH _ _ P L) => /=. - by rewrite (negbTE zDx) (negbTE zDy) E. - by rewrite -E -same_fconnect1_r. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)