proposition: Lemma refine_smatte_proper s m i E : proper_smatte m i E -> proper_smatte (refine_smatte s m) i E.
proof: Proof. case=> ri_m rm_ab; split=> [z /in_refine_smatte/ri_m//| e Ee]. by case/rm_ab=> // z [m_z ab_z]; exists z; split; first apply/in_refine_smatte. Qed.
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)