proposition: Lemma prefix_coloring_exists n : exists k, prefix_coloring n k.
proof: Proof. elim: n => /= [|n [k0 [n_k0 ext_k0 min_k0]]]. exists [map z1 z2 | False]; split=> // n. by have [k [kP k_n]] := pcoloring_exists n; exists k => // z1 z2 []. set n1 := n.+1; have le_nn1: n <= n1 := leqnSn n. without loss n1_n: / in_pmap n1 'z_n. apply: Rwlog => n1'n; have En1n z: in_pmap n1 z -> in_pmap n z. by case/in_pmapP=> i; rewrite leq_eqVlt => /predU1P[[->]|?] [] //; exists i. exists k0; split=> [z1 z2 /n_k0/(pmap_le le_nn1)// | i | n' i k']. have [k kP Ek0k] := ext_k0 i. by exists k => // z1 z2 /En1n-n_z1 /En1n-n_z2; apply: Ek0k. by rewrite leq_eqVlt => /predU1P[[->] _ [_ /cover_pmap[]] //|]; apply: min_k0. pose ext n0 j k := [/\ pcoloring n0 k, eq_pmap n k0 k & pmap n1 k 'z_j 'z_n]. pose limit_min j0 := exists2 n0, n < n0 & forall j k, ext n0 j k -> j0 <= j. have{ext_k0}: ~ limit_min n1. case=> n0 lt_nn0 min_n0; have [k [kP k_n0] eq_k0k] := ext_k0 n0. case/negP: (ltnn n); apply: (min_n0 n k). by do 2!split=> //; apply/k_n0/cover_pmap/(pmap_std lt_nn0 n1_n). elim: {1 3}n1 (leqnn n1) => [_ []|j0 IHj0 le_j0n min'j1]; first by exists n1. wlog{IHj0} [n0 lt_nn0 min_j0]: / limit_min j0 by apply: Rwlog; apply/IHj0/ltnW. have{min'j1} ext0P n': n0 <= n' -> exists2 k, pcoloring n' k & ext n0 j0 k. move=> le_n0n'; have lt_nn': n < n' := leq_trans lt_nn0 le_n0n'. apply: RcontraR min'j1 => ext'n'; exists n' => // j k [kP Ek0k] k_jn. have kPn0: pcoloring n0 k := pcoloring_le le_n0n' kP. rewrite ltn_neqAle (min_j0 j k) //. by apply: RcontraR ext'n'; case: eqP => // ->; exists k. have [k1 _ Dk1] := ext0P n0 (leqnn n0); pose k2 := pmap n.+1 k1. have Ek12: eq_pmap n.+1 k1 k2 by apply: eq_map_pmap. have m1P z: in_pmap n.+1 z -> exists2 j, j <= n & pmap n0 m0 z 'z_j. by case/in_pmapP=> j le_jn /(pmap_le lt_nn0); exists j. have n1j0 : in_pmap n1 'z_j0 by have [_ _ []] := Dk1. exists k2; split; first exact: sub_pmap_pmap; last first. have [_ Ek01 k2_j0n] := Dk1 => i j k le_i_n Ek2k i1k_ji ext_k. have Ek02: eq_pmap n k0 k2 := eq_pmap_trans Ek01 (eq_pmap_le le_nn1 Ek12). have Ek0k: eq_pmap i k0 k by apply: eq_pmap_trans (eq_pmap_le _ Ek02) Ek2k. have [Di | lt_i_n]: i = n \/ i < n by apply/predU1P; rewrite -leq_eqVlt. rewrite Di in i1k_ji Ek0k ext_k *; exists j0 => //. have [[k' k'P Ekk'] [n1j _ k_ji]] := (ext_k n0, i1k_ji). apply: (min_j0 j k'); split=> //; last by split; last apply/Ekk'. exact: eq_pmap_trans Ek0k (eq_pmap_le le_nn1 Ekk'). by case: (min_k0 i j k) => // j1 le_j1j /n_k0[]; exists j1; last apply/Ek02. move=> n'; have [|k3 k3P Dk3] := ext0P (maxn n0 n'); first exact: leq_maxl. suffices{k2 Ek12 k3P} Ek13: eq_pmap n.+1 k1 k3. have Ek23: eq_pmap n.+1 k2 k3 := eq_pmap_trans (eq_pmap_sym Ek12) Ek13. by exists k3; first apply/(pcoloring_le _ k3P)/leq_maxr. move=> z1 z2 /m1P[i1 le_i1n n0iz1] /m1P[i2 le_i2n n0iz2]. have [[_ n0i1 _] [_ n0i2 _]] := (n0iz1, n0iz2). without loss suffices ext_subpmap: k1 k3 Dk1 Dk3 / k1 z1 z2 -> k3 z1 z2. by split; apply: ext_subpmap. have{Dk1} [[k1P k1n0] Ek01 [_ _ k1j0n]] := Dk1. have{Dk3} [[k3P k3n0] Ek03 [_ _ k3j0n]] := Dk3. suffices{z1 z2 n0iz1 n0iz2} k13i: k1 'z_i1 'z_i2 -> k3 'z_i1 'z_i2. have [/k1n0-k1iz1 /k1n0-k1iz2] := (n0iz1, n0iz2). have [/k3n0-k3iz1 /k3n0-k3iz2] := (n0iz1, n0iz2). move/(map_transl k1P k1iz1)/(map_transr k1P k1iz2). by move/k13i/(map_transl k3P k3iz1)/(map_transr k3P k3iz2). without loss{k3n0} lt_i12: i1 le_i1n n0i1 i2 le_i2n n0i2 / i1 < i2. move=> IHi; have [lt_i12 | lt_i21 | -> _] := ltngtP i1 i2; first exact: IHi. by move/(map_sym k1P)/IHi/(map_sym k3P); apply. exact/k3n0/cover_pmap. have lt_i1n: i1 < n := leq_trans lt_i12 le_i2n. have n_i1: in_pmap n 'z_i1 := pmap_std lt_i1n n0i1. have Ek13: eq_pmap n k1 k3 := eq_pmap_trans (eq_pmap_sym Ek01) Ek03. have [-> k1i1n | lti2n]: i2 = n \/ i2 < n by apply/predU1P; rewrite -leq_eqVlt. apply/(map_transr k3P k3j0n)/Ek13/(map_transr k1P k1j0n)=> //. apply/(pmap_std _ n1j0)/(leq_ltn_trans _ lt_i1n)/(min_j0 i1 k1). by do 2!split=> //; apply: pmap_std n_i1. by move=> k1z12; apply/Ek13=> //; apply: pmap_std n0i2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)