proposition: Lemma sub_cm_bbox i : subpred (cm i) bb.
proof: Proof. rewrite /bb; set e := flatten _ => p mi_p. have{mi_p}: p \in e by apply/flatten_mapP; exists i; rewrite ?mem_enum. elim: e => //= q e IHe; rewrite inE => qe_p. by apply/in_extend_grect => /=; case: (p == q) qe_p. 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)