proposition: Lemma size_limit_coloring : at_most_regions nc limit_coloring.
proof: Proof. pose inmf n k (f : nat -> point) := forall i, i < n -> cover k (f i). pose injf n (k : map) f := forall i j, i < j -> j < n -> ~ k (f i) (f j). pose minsize n k := exists2 f, inmf n k f & injf n k f. without loss [f lim_f inj_limf]: / minsize nc.+1 limit_coloring. apply: Rwlog; move: limit_coloring => k; elim: nc => [|n IHn] nonmin_n. by exists std_point => z k_z; case: nonmin_n; exists (fun=> z) => [i|i []]. without loss [f k_f inj_fk]: / minsize n.+1 k. apply: Rwlog => /IHn[f kf_k]; exists f => z /(kf_k z)[i /ltP/leqW/ltP]. by exists i. exists f => z k_z; pose fz i := if i < n.+1 then f i else z. apply: RcontraR nonmin_n => kf'n; exists fz => [i _ | i j lt_ij le_j_n1]. by rewrite /fz; case: ifP => // /k_f. rewrite /fz (leq_trans lt_ij) //; have [|_ k_fiz] := ifP; first exact: inj_fk. by case: kf'n; exists i => //; apply/ltP/(leq_trans lt_ij). have [k kPn k_f]: exists2 k, is_prefix k & inmf nc.+1 k f. elim: {-2}nc.+1 (ltnSn nc) => [|n IHn] le_nnc. by have [k kP] := prefix_coloring_exists 0; exists k; first exists 0. have [k1 [n1 inj_k1f] k1_f] := IHn (leqW le_nnc). have [k2 [n2 k2Pn] k2_fn] := lim_f n le_nnc. have /orP[le_n12 | le_n21] := leq_total n1 n2. exists k2 => [|i]; [by exists n2 | rewrite ltnS leq_eqVlt]. by case/predU1P=> [->|/k1_f]; last apply: (prefix_coloring_le le_n12). exists k1 => [|i]; [by exists n1 | rewrite ltnS leq_eqVlt]. by case/predU1P=> [->|/k1_f]; first apply: (prefix_coloring_le le_n21) k2_fn. have{lim_f} [nk /prefix_pcoloring[[kP _ [fk fk_k]] _]] := kPn. pose s_spec n s := forall i (j := nth 0 s i), i < n -> j < nc /\ k (fk j) (f i). have{fk_k} [s Ls Ds]: exists2 s, size s = nc.+1 & s_spec nc.+1 s. elim: nc.+1 => [|n IHn] in f k_f s_spec {inj_limf} *; first by exists [::]. have [i lt_i_n|s Ls Ds] := IHn (fun i => f i.+1); first exact: k_f. have [|j /ltP-lt_j_nc k_fkj_f0] := fk_k (f 0); first exact: k_f. by exists (j :: s) => [|[|i] //]; [congr _.+1 | apply: Ds]. have{inj_limf} Us: uniq s. rewrite -(mkseq_nth 0 s) map_inj_in_uniq ?iota_uniq // Ls => i1 i2. rewrite !mem_iota /= => le_i1n le_i2n Esi12. without loss lt_i12: i1 i2 le_i1n le_i2n Esi12 / i1 < i2. by move=> IHi; case: (ltngtP i1 i2) => // /IHi->. have [[_ k_s_fi1] [_ k_s_fi2]] := (Ds i1 le_i1n, Ds i2 le_i2n). have [] := inj_limf i1 i2 lt_i12 le_i2n. by exists k => //; apply/(map_transl kP k_s_fi1); rewrite Esi12. have [s' Ls' Ds']: exists2 s', size s' = nc & s' =i [pred i | i < nc]. by exists (iota 0 nc) => [|i]; rewrite (size_iota, mem_iota). case/negP: (ltnn nc); rewrite -Ls -Ls'; apply: uniq_leq_size => // i. by case/(nthP 0); rewrite Ds' Ls => j /Ds[lt_j_nc _] <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)