proposition: Lemma switchE f : {in [predC (pred2 x y)], switch x y f =1 f}.
proof: Proof. move => z. rewrite !inE /switch/=. by do 2 (case (_ == _)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)