proposition: Lemma gm_disk_def i : {subset diskN (gmring i) <= [preim halfg \o val of cm i]}.
proof: Proof. move=> _ /hasP[nv ri_nv /connectP[s vDs ->]]; set v := finv _ _ in vDs *. have{ri_nv} mi_v: halfg (val v) \in cm i. have:= map_f val ri_nv; rewrite val_gmring // in_mring => /andP[mi_nv _]. rewrite -[val v]gnodeK halfg_face -val_gmnode ?(f_finv nodeI) //. by rewrite (fclosed1 gm_inner_closed) (f_finv nodeI) inE (sub_cm_bbox mi_nv). elim: s {nv}v mi_v vDs => //= v s IHs u mi_u /andP[/andP[r'u uCv]]; apply: IHs. rewrite -(mem_map val_inj) val_gmring // in_mring inE mi_u /= negbK in r'u. case/clinkP: uCv => [Du | <-]. rewrite -[val v]gnodeK halfg_face -val_gmnode -?Du //. by rewrite (fclosed1 gm_inner_closed) -Du inE (sub_cm_bbox mi_u). rewrite -[u]faceK gedge2 in r'u; rewrite -[val _]gnodeK halfg_face. by rewrite -val_gmnode // (fclosed1 gm_inner_closed) inE (sub_cm_bbox r'u). 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)