proposition: Lemma glink_fp_skip_edge : glink z z -> skip_edge =1 skip edgeI.
proof: Proof. rewrite /glink /= => zGz [x z'z]; apply: val_inj => /=. case: eqP zGz => [ez_z _ | _ /pred2P[nz_z | fz_z]]; first by case: eqP => // ->. by rewrite -(inj_eq nodeI) edgeK nz_z ifN. by rewrite -[in face (edge x) == z]fz_z (inj_eq faceI); case: (edge x == z). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)