proposition: Lemma fswitchC x y f : fconnect (switch x y f) =2 fconnect (switch y x f).
proof: Proof. apply: eq_fconnect. exact: switchC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)