fact: Definition ab_cm_proper ab cm e i (b := ab e) (m := cm i) := gr_proper b -> [/\ i \in e -> has (inset b) m & has b m -> i \in e].
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)