proposition: Lemma merge_cancel3 (x y : G) : cancel3 edge (switch x y node) (switch (finv face y) (finv face x) face).
proof: Proof. move => z /=. rewrite !f_finv //. case: (altP (edge z =P finv face y)) => [|A]. rewrite eqxx -{2}[y](f_finv faceI) => <-. exact: edgeK. case: (altP (edge z =P finv face x)) => [e_z|B]. by case: (altP (y =P x)) => [->|?]; rewrite ?eqxx -[z]edgeK e_z f_finv. rewrite !ifF ?edgeK //. - apply: contra_neqF A => /eqP <-. by rewrite finv_f. - apply: contra_neqF B => /eqP <-. by rewrite finv_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)