proposition: Lemma card_gmdart : #|gmdart| = (bbw * bbh * 2 + bbw + bbh).*2.
proof: Proof. have [w_gt0 h_gt0 [p0 bbE bbP]] := cm_bboxE. rewrite -addnA muln2 doubleD -(cardC gm_inner); congr (_ + _)%N. rewrite -garea_refine_rect -size_enum_grect cardE -(size_map val). apply/eqP; rewrite -uniq_size_uniq ?enum_grect_uniq // => [|d]. exact/dinjectiveP/(in2W val_inj). rewrite mem_enum_grect in_refine_rect; apply/idP/imageP=> [bb_d|[u ? -> //]]. by have Gd: d \in gmgrid; [rewrite gmgridE bb_d | exists (Gmdart Gd)]. pose bbc c := Gpoint (0 < c < 3)%N (1 < c)%N. pose w1 := bbw%:Z - 1; pose h1 := bbh%:Z - 1. pose bbp c z := Gpoint (nth 0 [:: z; w1; z] c) (nth z [:: 0; z; h1] c). pose bbd c z := (p0 + bbp c z%:Z) *+ 2 + bbc c. pose bbl c := if ~~ odd c then bbw else bbh. pose side c := [seq bbd c z | z <- iota 0 (bbl c)]. have <-: size (flatten [seq side c | c <- iota 0 4]) = (bbw + bbh).*2. by rewrite !size_cat !size_map !size_iota addn0 addnA addnn. rewrite cardE -(size_map (val \o gmedge)); apply/perm_size. apply/uniq_perm; first exact/dinjectiveP/(in2W (inj_comp val_inj _))/edgeI. have bbd_inj c: injective (bbd c). move=> e1 e2 /(congr1 halfg); rewrite !halfg_add2 => /addIr/addrI. by do 4!case: c => [[]// | c]; case. have hasn_side c1 c2: (c1 < c2 < 4)%N -> has [mem side c1] (side c2) = false. rewrite andbC => ltc; apply/hasPn=> _ /mapP[z2 _ ->]; apply/mapP=> -[z1 _]. by move/(congr1 oddg); rewrite !oddg_add2; case: c2 c1 ltc; do 6!case=> //. by rewrite !cat_uniq !cats0 !has_cat !map_inj_uniq ?iota_uniq ?hasn_side. move=> d; apply/imageP/flatten_mapP=> [[/= u G'u ->] | [c ltc /mapP[z ltz ->]]]. rewrite -[gedge u]halfgK; rewrite !inE -(gedge2 u) halfg_edge in G'u. have:= valP (edge u); rewrite gmgridE orbC -implyNb halfg_edge G'u /=. case/bbP=> x [y [Deu ubx uby]]; rewrite {}Deu -addrA in G'u *. pose c := index (oddg (gedge u)) (traject ccw 0 4). exists c; first by rewrite /c; case: oddgP. apply/mapP; exists (if ~~ odd c then x else y). by rewrite /c mem_iota; case: oddgP. rewrite {}/c /bbd /bbp; congr ((p0 + _) *+ 2 + _); last by case: oddgP. case: oddgP G'u; rewrite bbE ?addr0 ?ubx ?uby /= ?andbT /h1 /w1; do ?by rewrite andbC -lez_addr1 subrK ltW // subr_ge0 -eqn0Ngt => /eqP->. - by have [/idPn||->] := ltrgtP bbh%:Z; rewrite ?addrK // -leNgt lez_addr1. - by have [/idPn||->] := ltrgtP bbw%:Z; rewrite ?addrK // -leNgt lez_addr1. rewrite -[bbd c z]gedge2; set ed := gedge (bbd c z). suffices /andP[Ged]: (ed \in gmgrid) && ~~ bb (halfg ed) by exists (Gmdart Ged). rewrite mem_iota /= -ltz_nat in ltz; rewrite !inE in ltc. rewrite gmgridE andb_orl andbN gedge2 halfg_edge halfg_add2 oddg_add2 -!addrA. by case/or4P: ltc ltz => /eqP->; rewrite !bbE !addr0 ?addrK ?ltxx => ->; rewrite ?gtr_addl !andbT ?subr_ge0. 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)