proposition: Lemma gmgridE d : (d \in gmgrid) = bb (halfg d) || bb (halfg (gedge d)).
proof: Proof. rewrite mem_cat -[d in d \in map _ _]gedge2 (mem_map (can_inj gedge2)). by rewrite !mem_enum_grect !in_refine_rect. 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)