proposition: Lemma approx_point_exists s z : exists p, approx_point s z p.
proof: Proof. case: z => x y. have [[mx Hmx] [my Hmy]] := (approx_exists s x, approx_exists s y). by exists (Gpoint mx my). 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)