proposition: Lemma cpcolor1U_correct f : (forall k', coloring k' -> @cp_extcol cp1 (CpU :: cp2) f k') -> cp_extcol (CpU :: cp1) (cpcolor1 CpU f) k.
proof: Proof. rewrite /cpmap -/cpmap -/G2; have [kE kF] := col_k. pose k' e u := oapp k (e +c k (node G2)) [pick x | cface u (icpU G2 x)]. have k'F e: invariant face (k' e) =1 ecpU G2. move=> u; apply/eqP; congr (oapp k _ _). by apply: eq_pick => v; rewrite -cface1. have{kF} k'G2 e x: k' e (icpU G2 x) = k x. rewrite /k' -(@eq_pick _ (cface x)) => [|y]; last by rewrite cface_icpU. by case: pickP => [y /fconnect_invariant-> | /(_ x)/idP]. have k'X e: k' e (ecpU G2) = e +c k (node G2). by rewrite /k'; case: pickP => // x; rewrite cface_ecpU. have k'Xe e: k' e (edge (ecpU G2)) = k (node G2). by rewrite -(k'G2 e) -(eqcP (k'F e _)). have{kE} k'col e: e != Color0 -> coloring (k' e). move=> nz_e; have k'EX: invariant edge (k' e) (ecpU G2) = false. by rewrite /= k'X k'Xe addcC -addc_eq0 addKc (negPf nz_e). split=> // [] [||x] //=; first by rewrite eq_sym. by rewrite (k'G2 _ (edge _)) k'G2; apply: kE. have Dk' e: trace (map (k' e) (cpring (ecpU G2))) = [:: e, e & et]. rewrite cpring_ecpU !map_cons k'X k'Xe addcC -map_comp (eq_map (k'G2 e)). by rewrite /= addKc /et head_cpring /= addcC /ctrace /= !addKc. move/(_ _ (k'col _ _))=> f_col. have []/= := f_col Color3; have []//:= f_col Color2; have []// := f_col Color1. rewrite !Dk' /= -/G2; set h := cp_ht0 _ _ => t1ok t1P t2ok t2P t3ok t3P. split; first by do !apply: ctree_union_proper. rewrite !(@ctree_mem_union h) //; last exact: ctree_union_proper. apply: (iffP or3P) => [|[k0 k0ccol Dk]]. by case=> [/t1P|/t2P|/t3P] [k0 ? Dk0]; exists k0 => // x; rewrite [_ x]Dk0. have [k0col _] := k0ccol; pose ic2 := @injcp cp1 (CpU :: cp2). pose e0 := k0 (ic2 (ecpU G2)) +c k (node G2). have k0G: k0 \o ic2 =1 k' e0. rewrite /= -/G2 => u /=; have [[x xFu] | XFu] := @fband_icpU _ G2 u. by rewrite (fconnect_invariant (k'F e0) xFu) k'G2 -Dk; apply: gcol_cface. rewrite -(fconnect_invariant (k'F e0) XFu) k'X -addcA addcc addc0. exact/esym/gcol_cface. case De0: e0 in k0G; [ idtac | by constructor 1; apply/t1P; exists k0 | by constructor 2; apply/t2P; exists k0 | by constructor 3; apply/t3P; exists k0 ]. case/andP: (@gcol_adj _ (CpU :: cp2) _ k0col _ _ (@adj_ecpU G2 G2)) => /eqP[]. by rewrite ![k0 _]k0G k'G2 k'X add0c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)