proposition: Lemma cpcolor1A_correct f : (forall k', coloring k' -> @cp_extcol cp1 (CpA :: cp2) f k') -> cp_extcol (CpA :: cp1) (cpcolor1 CpA f) k.
proof: Proof. rewrite /cpmap -/cpmap -/G2; have [De12 | neq_e12] := eqVneq e1 e2; last first. split; rewrite /cpcolor1 -/G2 -/et Det /et1 (negPf neq_e12) //. right; move=> [k0 [[_ k0F] _] Dk]; case/eqP: neq_e12. rewrite /e1 addcC; congr addc; rewrite -!Dk; apply: (fconnect_invariant k0F). apply: (sub_cface_injcp cp1); rewrite (cface_icpA G2) /=. by rewrite !unfold_in /= !connect0 !orbT. pose k' : ecpA G2 -> color := k; have [kE kF] := col_k. have:= De12; rewrite [e1]addcC => /addcI KnG. have k'F: invariant face k' =1 ecpA G2. move=> x; apply/eqP; move: (fconnect1 face x); rewrite cface_icpA /k'. case/orP=> [/fconnect_invariant <-// | /allP kFx]. have {}kFx y: y \in [:: x; face x] -> k y = k (node G2). move/kFx; rewrite /= unfold_in => /hasP[z Dz /fconnect_invariant-> //]. by move: Dz; rewrite !inE => /pred2P[]->. by rewrite /= kFx ?(kFx x) // ?inE ?eqxx ?orbT. have k'col: coloring k'. split=> // x; rewrite /= /ecpA_edge if_neg. case: ifP => eGFnG; last exact: kE. case: (x =P _) => [-> | _]. rewrite /k' -(eqcP (kF _)) nodeK eq_sym -{1}(nodeK G2) (eqcP (kF _)). exact: kE. case: (x =P _) => [Dx|_]; last by apply: kE. rewrite -(canLR (@nodeK G2) Dx) -cface1r in eGFnG. by rewrite /k' (fconnect_invariant kF eGFnG); apply: kE. case/(_ _ k'col); rewrite /cpmap -/cpmap -/G2. suffices ->: trace (map k' (cpring (ecpA G2))) = if et2 is nil then et else et2. by move=> t_ok tP; split; rewrite /= /k' -/et Det /et1 -/et1 -Det De12 eqxx. rewrite /k' cpring_ecpA; case: ifP => G2gt2. rewrite -urtrace_trace /et2 (head_long_cpring G2gt2) /= rot1_cons -KnG. by rewrite /urtrace last_rcons -map_rcons headI. by rewrite -/et /et2 drop_oversize // leqNgt -size_long_cpring G2gt2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)