proposition: Lemma cpcolor1K_correct f : (forall k', coloring k' -> @cp_extcol cp1 (CpK :: cp2) f k') -> cp_extcol (CpK :: cp1) (cpcolor1 CpK f) k.
proof: Proof. rewrite /cpmap -/cpmap -/G2; have [kE kF] := col_k. pose k' u := oapp k Color0 [pick x | cface u (icpK G2 x)]. have k'F: invariant face k' =1 ecpK G2. move=> u; apply/eqP; congr (oapp _ _). by apply: eq_pick => v; rewrite -cface1. have k'G2 x: k' (icpK G2 x) = k x. rewrite /k' -(@eq_pick _ (cface x)) => [|y]; last by rewrite cface_icpK. by case: pickP => [y /fconnect_invariant-> | /(_ x)/idP]. pose ic2 := @injcp cp1 (CpK :: cp2). case eq_e12: (e1 == e2). split; rewrite /= -/et Det /et1 eq_e12 //; right=> [] [k0 [[k0E k0F] _] Dk]. rewrite /e1 /e2 addcC (inj_eq (addcI _)) in eq_e12. have nGAfeG: adj (ic2 (icpK G2 (node G2))) (ic2 (icpK G2 (face (edge G2)))). by apply: sub_adj_injcp; rewrite (adj_icpK G2) fconnect1 connect0 !orbT. have [u nGFu uRfeG] := adjP nGAfeG; case/eqcP: (k0E u). rewrite -(fconnect_invariant k0F nGFu) (fconnect_invariant k0F uRfeG). by rewrite ![k0 _]Dk (eqP eq_e12). have k'col: coloring k'. rewrite /e1 /e2 addcC (inj_eq (addcI _)) (eqcP (kF (edge G2))) in eq_e12. split=> // u /=. have [[x uFx] [y euFy]] :=(fband_icpK u, fband_icpK (edge u)). rewrite (fconnect_invariant k'F uFx) (fconnect_invariant k'F euFy) !k'G2. have xAy: adj (icpK G2 x) (icpK G2 y). by apply/adjP; exists u; first by rewrite cfaceC. rewrite adj_icpK in xAy; case/or3P: xAy. - case/adjP=> z xFz zRy; rewrite (fconnect_invariant kF xFz). by rewrite -(fconnect_invariant kF zRy); apply: kE. - case/andP=> eGFx nGFy; rewrite -(fconnect_invariant kF eGFx). by rewrite -(fconnect_invariant kF nGFy). case/andP=> eGFy nGFx; rewrite -(fconnect_invariant kF nGFx). by rewrite -(fconnect_invariant kF eGFy) eq_sym. case/(_ _ k'col); rewrite /cpmap -/cpmap -/G2. have <-: e1 +c e2 :: et2 = trace (map k' (cpring (ecpK G2))). rewrite cpring_ecpK !map_cons -map_comp (eq_map k'G2). rewrite (fconnect_invariant k'F (cface_node_ecpK G2)) k'G2. move/esym: Det; rewrite /et drop_behead (head_proper_cpring G2gt1). rewrite map_cons -!urtrace_trace /urtrace !rot1_cons !last_rcons /=. by rewrite headI /= /et1 => [] [De2 <-]; rewrite /e1 De2 -addcA addKc. move=> t_ok tP; split; rewrite /cpcolor1 -/G2 -/et Det /et1 eq_e12 {t_ok}//. apply: (iffP tP) => {tP} [] [k0 k0ccol Dk]; have [k0col _] := k0ccol. by exists k0 => // x; rewrite [_ x]Dk k'G2. exists k0 => // u; have [x uFx] := fband_icpK u. by rewrite /= (fconnect_invariant k'F uFx) k'G2 -Dk; apply: gcol_cface. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)