proposition: Lemma pmap_finite n : finite_simple_map (pmap n m0).
proof: Proof. split; last first. exists n, std_point => z [n_z [i lt_i_n m0zi] _]; exists i; first exact/ltP. by split; [apply/(in_pmap_trans n_z) | | apply/(map_sym m0P)]. split; first exact: (pmap_plain n m0P). move=> z1 z2 [n_z1 n_z2 m0z12]. have [r r_z2 m0_r] := simple_map_open m0P m0z12. by exists r => // z /m0_r-m0z1z; split=> //; apply: in_pmap_trans m0z1z. move=> z r1 r2 r1P r2P r12_nz [z1 [r1z1 [n_z _ m0zz1]]] [z2 [r2z2 [_ _ m0zz2]]]. have []: meet r1 (m0 z) /\ meet r2 (m0 z) by split; [exists z1 | exists z2]. apply: simple_map_connected => // t m0zt. by have n_t: in_pmap n t := in_pmap_trans n_z m0zt; apply/r12_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)