proposition: Lemma base_skip_edge : @fun_base G G' val edge edge (pred2 (node fz) nz).
proof: Proof. move=> u v /=; rewrite -val_eqE /= -(canF_eq edgeK) => /norP[/negPf-> nz'u]. by rewrite (canF_eq (canF_sym nodeK)) (negPf nz'u) if_same. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)