proposition: Lemma limit_coloring_coloring : coloring m0 limit_coloring.
proof: Proof. split=> [|z [k [n [n_k _ _]] /n_k[/cover_pmap[]]] //||]; last 1 first. - by move=> z1 z2 adj_z12 [k [n /prefix_pcoloring[[_ /(_ z1 z2 adj_z12)]]]]. - split=> z1 z2 [k1 [n1 k1Pn] k1z12] => [|z3 [k3 [n3 k3Pn] k3z23]]. have [k1P _] := prefix_pcoloring k1Pn. by exists k1; [exists n1 | apply/(map_sym k1P)]. have [k kPn [k_z12 k_z23]]: exists2 k, is_prefix k & k z1 z2 /\ k z2 z3. case/orP: (leq_total n1 n3) => /prefix_coloring_le => [sub_k13 | sub_k31]. by exists k3; [exists n3 | split; first apply: sub_k13 k1z12]. by exists k1; [exists n1 | split; last apply: sub_k31 k3z23]. have [_ /prefix_pcoloring[kP _]] := kPn. by exists k => //; apply/(map_trans kP k_z12). move=> z1 z2 m0z12; have [m0z1 m0z2] := map_cover m0P m0z12. have [[i1 m0iz1] [i2 m0iz2]] := (has_std_point m0z1, has_std_point m0z2). have [n lt_i1n lt_i2n]: exists2 n, i1 < n & i2 < n. by exists (maxn i1 i2).+1; rewrite ltnS (leq_maxl, leq_maxr). have [k kPn] := prefix_coloring_exists n; exists k; first by exists n. by have [kP] := prefix_pcoloring kPn; apply; split; [exists i1 | exists i2 | ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)