proposition: Lemma base_clink_Walkup : @rel_base G G' val clink clink (pred2 (edge nz) nz).
proof: Proof. move=> u v /norP[]; rewrite -(canF_eq faceK) => z'fu nz'u. rewrite !(sameP clinkP pred2P) -!val_eqE /= (negbTE z'fu); congr (_ || _). by case: (_ =P z) => // ->; rewrite z'G' (negbTE nz'u). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)