proposition: Lemma switchxx x f : switch x x f =1 f.
proof: Proof. move => z /=. by case (altP (z =P x)) => [->|]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)