fact: Definition proper_smatte (m : smatte) i (E : pred Er) := let meet_m be := gr_proper be.2 -> meet m (inset_srect be) in subregion m (m0 (mr i)) /\ {in E, forall e, meet_m (ab e)}.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph bigop ssralg ssrnum ssrint) mathcomp(div intdiv) fourcolor(hypermap geometry coloring grid matte gridmap) fourcolor(real realplane realprop approx)