proposition: Lemma mem_approx_refine s (gr : gregion) z : mem_approx s.+1 (preim halfg gr) z <-> mem_approx s gr z.
proof: Proof. split=> [] [p Dp Hp]; first by exists (halfg p); first apply/approx_halfg. have [q Dq] := approx_point_exists s.+1 z; exists q => //=. by rewrite (approx_point_inj (approx_halfg Dq) Dp). 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)