proposition: Lemma can_switch : cancel xswitch (switch (f y) (f x) (finv f)).
proof: Proof. move => z; case: (altP (x =P y)) => [->|xDy]; rewrite ?switchxx ?finv_f //=. case: (altP (z =P x)) => [->|zDx]; first by rewrite eqxx finv_f. case: (altP (z =P y)) => [->|zDy]; first by rewrite (inj_eq inj_f) (negbTE xDy) eqxx finv_f. by rewrite !(inj_eq inj_f) ?(negbTE zDy) ?(negbTE zDx) ?eqxx finv_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)