proposition: Lemma prefix_coloring_le n1 n2 k1 k2 : n1 <= n2 -> prefix_coloring n1 k1 -> prefix_coloring n2 k2 -> submap k1 k2.
proof: Proof. move=> le_n12 k1pre k2pre; have [n1k1 _ _] := k1pre. without loss{n2 le_n12 k2pre} k2pre: k2 / prefix_coloring n1 k2. have [[n2k2 k2_ext k2_min] [k2P _]] := (k2pre, prefix_pcoloring k2pre). move=> IHn2 _ _ /(IHn2 (pmap n1 k2))[] //. split; [exact: sub_pmap_pmap | exact: pmap_extensible k2_ext |]. move=> i j k lt_i_n1 Ek2k i1k_ji k_ext. case: (k2_min i j k) => // [||j0 le_j0j k2j0i]; first exact: leq_trans le_n12. exact/(eq_pmap_trans _ Ek2k)/(eq_pmap_le (ltnW lt_i_n1))/eq_map_pmap. have [i1j i1i _] := i1k_ji; have n1i := pmap_std lt_i_n1 i1i. have [/n2k2[n2j0 _ _] k2i] := map_cover k2P k2j0i. have [le_i_j | lt_j_i] := leqP i j; first by exists i. have lt_j0_n1: j0 < n1 := leq_ltn_trans le_j0j (ltn_trans lt_j_i lt_i_n1). by exists j0 => //; split=> //; apply: pmap_std lt_j0_n1 n2j0. suffices Ek12: eq_pmap n1 k1 k2 by move=> z1 z2 /n1k1[nz1 nz2 k1z]; apply/Ek12. elim: {-2}n1 (leqnn n1) => /= [|n IHn] lt_nn1 z1 z2; first by case. have m1P z: in_pmap n.+1 z -> exists2 i, i <= n & pmap n1 m0 z 'z_i. by case/in_pmapP=> i le_i_n n1zi; exists i; last apply: pmap_le n1zi. move/(_ (ltnW lt_nn1)) in IHn => /m1P[i1 le_i1n n1iz1] /m1P[i2 le_i2n n1iz2]. without loss suffices{n1k1} IHk: k1 k2 k1pre k2pre IHn / k1 z1 z2 -> k2 z1 z2. by split; apply: IHk => //; apply/eq_pmap_sym. have [[k1P k1n1] [_ n1i1 _]] := (prefix_pcoloring k1pre, n1iz1). have [[k2P k2n1] [_ n1i2 _]] := (prefix_pcoloring k2pre, n1iz2). suffices{z1 n1iz1 z2 n1iz2} k12i: k1 'z_i1 'z_i2 -> k2 'z_i1 'z_i2. have [/k1n1-k1iz1 /k1n1-k1iz2] := (n1iz1, n1iz2). have [/k2n1-k2iz1 /k2n1-k2iz2] := (n1iz1, n1iz2). move/(map_transl k1P k1iz1)/(map_transr k1P k1iz2). by move/k12i/(map_transl k2P k2iz1)/(map_transr k2P k2iz2). without loss lt_i12: i1 i2 le_i1n le_i2n n1i1 n1i2 / i1 < i2. move=> IHi; have [lt_i12 | lt_i21 | -> _] := ltngtP i1 i2; first exact: IHi. by move/(map_sym k1P)/IHi/(map_sym k2P); apply. exact/k2n1/cover_pmap. have [lt_i1n1 lt_i2n1]: i1 < n1 /\ i2 < n1 by split; apply: leq_trans lt_nn1. have lt_i1n: i1 < n by apply: leq_trans lt_i12 le_i2n. case: (ltngtP i2) le_i2n => // [lt12n|Di2] _. by move/IHn; apply; [apply: pmap_std n1i1 | apply: pmap_std n1i2]. rewrite {i2}Di2 in n1i2 lt_i12 {le_i1n lt_i2n1} * => k1i1n. elim: {1}n i1 lt_i12 => // n3 IHn3 i1 lt_i1n3 in lt_i1n {lt_i1n1} n1i1 k1i1n *. have [[n1k1 k1ext k1min] [n1k2 k2ext k2min]] := (k1pre, k2pre). have [n'_i1 n'_n] := (pmap_std (leqW lt_i1n) n1i1, pmap_std (ltnSn n) n1i2). have /(k2min n i1)[//|//|//|i3] := pmap_extensible lt_nn1 k1ext. exact/(eq_pmap_trans (eq_pmap_sym IHn))/(eq_pmap_le (leqnSn n))/eq_map_pmap. rewrite leq_eqVlt => /predU1P[-> // | lt_i31] k2i3n. have lt_i3n: i3 < n by apply: ltn_trans lt_i1n. have n'i3: in_pmap n.+1 'z_i3 by have /n1k2[/(pmap_std (leqW lt_i3n))] := k2i3n. have /(k1min n i3)[//|//|//|i4 le_i43 k1i4n] := pmap_extensible lt_nn1 k2ext. exact/(eq_pmap_trans IHn)/(eq_pmap_le (leqnSn n))/eq_map_pmap. have lt_i4n: i4 < n by apply: leq_trans lt_i3n. have lt_i4n3: i4 < n3 by apply: (leq_trans (leq_ltn_trans le_i43 lt_i31)). have n1i4: in_pmap n1 'z_i4 by case/n1k1: k1i4n. have: k2 'z_i4 'z_n by [apply/IHn3]; apply: (map_trans k2P). by apply/IHn/(map_transr k1P k1i4n)=> //; apply/(@pmap_std _ n1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)