proposition: Lemma mem_approx_refine_inset s (b : grect) : subregion (mem_approx s (inset b)) (mem_approx s.+1 (inset (refine_rect b))).
proof: Proof. move=> z /mem_approx_refine[p Dp]; rewrite /= -in_refine_rect refine_inset. by move/insetW; exists p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple path fingraph bigop order ssralg) mathcomp(ssrnum ssrint div intdiv) fourcolor(hypermap geometry coloring grid matte) fourcolor(real realplane) Coq(Setoid Morphisms) fourcolor(realsyntax realprop)