proposition: Lemma eq_mem_approx s (gr1 gr2 : gregion) z : gr1 =1 gr2 -> (mem_approx s gr1 z <-> mem_approx s gr2 z).
proof: Proof. by move=> Dgr; split; apply/sub_mem_approx=> p; rewrite Dgr. 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)