proposition: Lemma pcoloring_exists n : exists k, pcoloring n k.
proof: Proof. have [k [kP n_k k_n adj'k] nc_k] := fin_colorable (pmap_finite n). have clos_n z t: in_pmap n z -> closure (m0 z) t -> closure (pmap n m0 z) t. move=> n_z m0zt r rP r_t; have [u [m0zu r_u]] := m0zt r rP r_t. by exists u; do !split => //; apply: in_pmap_trans m0zu. exists k; do 2![split=> //]=> z1 z2 [m0'z12 [z [[f fP] [z1z z2z]]] kz12]. have [/n_k[n_z1 _ _] /n_k[n_z2 _ _]] := map_cover kP kz12. apply: adj'k kz12; split=> [/pmap_sub//|]; exists z. split; [exists f => t [[_ n_t m0t] m0tz] | by split; apply/clos_n]. have /fP[i lti2 [m0it m0iz]]: cover (corner_map m0 z) t. by split=> // r rP /(m0tz r rP)[u [/pmap_sub-m0tu r_u]]; exists u. have n_i: in_pmap n (f i) by apply/(in_pmap_trans n_t)/(map_sym m0P). by exists i => //; split=> //; apply: clos_n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)