proposition: Lemma gmdart_connected : connected gmdart_map.
proof: Proof. have [w_gt0 h_gt0 [p0 bbE bbP]] := cm_bboxE. have[:uP] @u := @Gmdart ((p0 + 0) *+ 2) uP. by rewrite gmgridE halfg_double bbE w_gt0 h_gt0. apply/eqP; congr (_ = 1%N): (n_comp_connect glinkC u). apply/eq_n_comp_r => /= v; rewrite !inE glinkC. without loss bb_v: v / v \in gm_inner. have:= valP v; rewrite gmgridE => /orP[bb_v | bb_ev] IHv; first exact: IHv. by rewrite (same_connect1 glinkC (glinkE v)) IHv. have /bbP[x [] y [] Dv _ _] := bb_v. move Dn: (x + y).+1 => n; elim: n => // n IHn in x y v Dv bb_v Dn *. without loss Dov: v Dv bb_v / oddg v = oddg (Gpoint 0 (x != 0%N)). set c := (c in oddg c) => IHv; move: Dv; rewrite -[RHS](halfg_eq _ (oddgP c)). case/esym/same_halfg/trajectP=> i _ Dv; elim: i => [|i IHi] in v Dv bb_v *. by rewrite IHv ?Dv ?halfg_eq ?oddg_eq. rewrite (same_connect1 glinkC (glinkN v)) IHi ?gm_inner_node //. by rewrite val_gmnode // Dv gfaceK. case: n IHn => [_|n IHn] in Dn. apply/eq_connect0/val_inj; rewrite -[val v]halfgK {}Dv {}Dov. by case: x y Dn => -[] _ //; rewrite addr0. have{Dov} Dev: halfg (gmedge v) = p0 + Gpoint (x - 1)%N (y - (x == 0))%N. by rewrite halfg_edge {}Dv {}Dov addrAC -addrA; case: x y Dn => [|x] []. rewrite (same_connect1 glinkC (glinkE v)) (IHn _ _ _ Dev) //. have:= bb_v; rewrite !inE Dv Dev !bbE /= => /andP[ubx uby]. by rewrite !ltz_nat !(leq_ltn_trans (leq_subr _ _)). by case: x y {Dv Dev} Dn => [|x] [|y] // [<-]; rewrite !subn1. 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)