proposition: Lemma fcard_gmface : fcard face gmdart_map = (bbw.+1 * bbh.+1)%N.
proof: Proof. have [w_gt0 h_gt0 [p0 bbE bbP]] := cm_bboxE. pose gmframe := enum_grect (Grect 0 bbw.+1 0 bbh.+1). have gmendP (u : gmdart): end0g u - p0 \in gmframe. without loss /bbP[x [] y [] Du ubx uby]: u / u \in gm_inner. move=> IHu; have:= valP u; rewrite gmgridE => /orP[/IHu//|]. rewrite -halfg_face -[gface _]gnode4 gedgeK => bbn3u; have:= IHu (face u). by rewrite inE val_insubd gmgridE bbn3u !end0g_node => ->. rewrite /end0g {}Du addrC -addrA addKr mem_enum_grect !intS !(addrC 1). by case: oddgP; rewrite /= ?addr0 ?ltr_add2r ?ltz_addr1 ?ltW ?ubx. pose gmend u := SeqSub (gmendP u). suffices adj_gmend: fun_adjunction gmend id face predT. rewrite -(adjunction_n_comp _ (fconnect_sym _) cfaceC _ adj_gmend) //. rewrite fcard_id card_seq_sub ?enum_grect_uniq // size_enum_grect /=. by rewrite /garea /= /zwidth !addr0. split=> [[[x y] Gxy] _ | u v _]; last first. by rewrite fconnect_id cface_end0g eq_sym -val_eqE /= (inj_eq (addIr _)). pose c := locked Gpoint (x == bbw) (y == bbh). suffices Gu: (p0 + (Gpoint x y - oddg c)) *+ 2 + oddg c \in gmgrid. exists (Gmdart Gu); rewrite fconnect_id -val_eqE /= addrCA -addrA -opprB. by rewrite halfg_eq ?oddg_eq ?subrK. rewrite gmgridE halfg_eq //= {}/c -lock bbE !ltr_subl_addl !subr_ge0. apply/orP; left; apply/andP; move: Gxy; rewrite mem_enum_grect /=. rewrite !intS !ltz_add1r (le_eqVlt x) (le_eqVlt y) => /andP[Gx Gy]. by split; [move: Gx | move: Gy]; case: eqP => // -> _; rewrite ltr_addr andbT. 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)