proposition: Lemma skip_edgeK : cancel3 skip_edge (skip nodeI) (skip faceI).
proof: Proof. case=> x z'x; apply/val_inj; rewrite /= !(canF_eq edgeK). have /altP[fex_z | z'fex] := face (edge x) =P z. have nz_x: nz = x by rewrite -fex_z edgeK. rewrite ifT //; case z_nfz: (z == _); first by rewrite fex_z eqxx eq_sym. by rewrite ifN_eqC ?edgeK // -(canF_eq nodeK) nz_x. case: (z == _); first by rewrite (negPf z'fex) edgeK ifN. have [x_nfz | _] := x =P node fz; first by rewrite nodeK eqxx -x_nfz ifN. by rewrite (negPf z'fex) edgeK ifN. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)