proposition: Lemma has_std_point z : cover m0 z -> exists i, m0 z 'z_i.
proof: Proof. move=> m0z; have [rr rrz m0rr] := simple_map_open m0P m0z. have [b [p p_z /insetW-b_p] rr_b] := approx_rect rrz. set s := _.1 in p_z; exists (pickle (s, p)); rewrite /std_point pickleK /=. exact/m0rr/rr_b/mem_approx_scale. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)