proposition: Lemma ab_mr_proper_refine s b e i : ab_mr_proper b e i -> ab_mr_proper (refine_srect s b) e i.
proof: Proof. rewrite /ab_mr_proper gr_proper_refine => beiP /beiP{beiP}[ei_b b_ei]. split=> [/ei_b|] [z []]; first by exists z; split; first apply/in_refine_inset. by move/in_refine_srect=> b_z m0i_z; apply/b_ei; exists z. 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)