proposition: Lemma switchK f : switch x y (switch x y f) =1 f.
proof: Proof. move => z. case: (altP (x =P y)) => [<-|xDy]; rewrite ?switchxx //= ?eqxx. case: (altP (z =P x)) => [->|zDx]. - by rewrite [_ == x]eq_sym (negbTE xDy). - by case: (altP (z =P y)) => // ->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)