proposition: Lemma grid_map_coloring : four_colorable grid_map -> exists k : Ir -> 'I_4, forall e, gr_proper (ab0 e) -> k e.1 != k e.2.
proof: Proof. rewrite /grid_map; case: has_cutout => G h r planG Ih hE _ hN Dr cycNr. case/four_colorable_dual=> k [kE /fconnect_invariant-kN]. have{cycNr kN} k_r i: {in r i &, forall x y, k x = k y}. by have /andP[/fconnect_cycle-cycNri _] := cycNr i isT => x y /cycNri<- /kN. pose kn x := Ordinal (index_size (k x) [:: Color0; Color1; Color2] : _ < 4)%N. exists (fun i => oapp kn ord0 [pick x in r i]) => e /ab_cmP/hasP[d]. rewrite !inE eqE /= -!val_gmring => /mapP[u r2u {d}->] /mapP[eu r1eu Deu]. have {}Deu: edge u = eu by apply/val_inj. rewrite -{eu}Deu -!{}Dr !mem_rev in r2u r1eu. case/mapP: r2u r1eu => x r2x ->; rewrite -hE mem_map // => r1ex. apply: contraFN (kE x); have [y /= /k_r <- | /(_ (edge x))/idP] // := pickP. by have [z /(k_r _ x)-> | /(_ x)/idP] //= := pickP; do 2!case: (k _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph order ssralg ssrnum ssrint) fourcolor(hypermap geometry color coloring patch snip grid) fourcolor(matte)