proposition: Lemma approx_halfg s z p : approx_point s.+1 z p -> approx_point s z (halfg p).
proof: Proof. by case: z p => [x y] [mx my] [Hx Hy]; split; apply: approx_halfz. 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)