proposition: Lemma cm_bboxE : [/\ 0 < bbw%:Z, 0 < bbh%:Z & exists2 p0, forall x y, bb (p0 + Gpoint x y) = (0 <= x < bbw) && (0 <= y < bbh) & forall p, bb p -> exists x y : nat, [/\ p = p0 + Gpoint x y, x%:Z < bbw & y%:Z < bbh]].
proof: Proof. have [w_gt0 h_gt0]: 0 < bbw%:Z /\ 0 < bbh%:Z; last split=> //. apply/andP; rewrite -muln_gt0; apply: garea_subrect grect0 bb _ => p r0p. rewrite /bb; elim: (flatten _) => //= q e IHe. by rewrite in_extend_grect //= IHe orbT. case: bb w_gt0 h_gt0 => x0 x1 y0 y1 /=; rewrite -[x1](subrK x0) -[y1](subrK y0). rewrite /zwidth /= !addrK; case: (_ - _) (_ - _) => h []w _ _ //. pose p0 := Gpoint x0 y0; exists p0 => [x y | p]. by rewrite addrC /= !ltr_add2r !ler_addr. rewrite -(subrK p0 p); case: (p - p0) => x y /=; rewrite !ler_addr !ltr_add2r. by case: x y => x [] y /andP[] //; exists x, y; first rewrite addrC. 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)