proposition: Lemma val_gmring i : map val (gmring i) = mring (cm i).
proof: Proof. rewrite (pmap_filter (insubK _)) (all_filterP _) //. apply/allP=> d; rewrite in_mring => /andP[mi_d _]. by rewrite isSome_insub gmgridE (sub_cm_bbox mi_d). 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)