proposition: Lemma fconnect_switchV z : fconnect f z x -> fconnect xswitch z x || fconnect xswitch z y.
proof: Proof. move => fc_zx; case: (boolP (fconnect (switch x y f) z x)) => //=. case/connectP : (fc_zx) => p; elim: p z fc_zx => /= [? _ _ <- //|]; first by rewrite connect0. have ? := switch_inj; move => a p IHp z fc_zx /andP [/eqP<- P1 P2] sw_zx. wlog zDxy : / z \in [predC pred2 x y]. { move => W; case: (altP (z =P y)) => [-> //|zDx]; apply: W; rewrite !inE (negbTE zDx) orbF. by apply: contraNneq sw_zx => ->. } rewrite same_fconnect1 ?switchE // in sw_zx. by rewrite same_fconnect1 ?switchE ?IHp // -?same_fconnect1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)