proposition: Lemma mem_approx_scale s gr p : reflect (mem_approx s gr (scale_point s p)) (gr p).
proof: Proof. apply: (iffP idP) => [Hp | [p' Dp' Hp']]. by exists p; first by apply approx_scale_point. by rewrite (approx_point_inj (approx_scale_point _ _) 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)