proposition: Lemma approx_point_inj s z p1 p2 : approx_point s z p1 -> approx_point s z p2 -> p1 = p2.
proof: Proof. case: z p1 p2 => [x y] [mx1 my1] [mx2 my2] [Hx1 Hy1] [Hx2 Hy2]. by congr (Gpoint _ _); eapply approx_inj; eauto. 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)