proposition: Lemma cpcolor1_correct cp1 cp2 k : coloring k -> @cp_extcol cp1 cp2 (foldr cpcolor1 cpbranch cp1) k.
proof: Proof. move=> col_k; rewrite -(revK cp1); move/rev: cp1 => cp1. pose ecp1 := rev (cpexpand cp1). suffices []: cp_extcol ecp1 (foldr cpcolor1 cpbranch ecp1) k. rewrite {}/ecp1 -cpcolor1_cpexpand_rev ?memc0_trace_cpring // => t_ok tP. split; last by move: tP; rewrite /cp_tr0; case: (injcp_expand cp1 cp2). by move: t_ok; rewrite /cp_ht0 -!size_ring_cpmap; case: injcp_expand. rewrite {}/ecp1; elim/last_ind: cp1 cp2 k col_k => [|cp1 s IHcp] cp2 k col_k. by apply: cpbranch_correct. rewrite cpexpand_rcons rev_cat; case: s => [n||||||] /=. - by apply: cpcolor1R_correct => //; apply: IHcp. - by apply: cpcolor1R'_correct => //; apply: IHcp. - apply: cpcolor1U_correct => // k1 k1col. apply: cpcolor1R_correct => // k2 k2col. apply: cpcolor1K_correct => // k3 k3col. by apply: cpcolor1R'_correct => //; apply: IHcp. - apply: cpcolor1U_correct => // k1 k1col. apply: cpcolor1R_correct => // k2 k2col. apply: cpcolor1K_correct => // k3 k3col. apply: cpcolor1K_correct => // k4 k4col. by apply: cpcolor1R'_correct => //; apply: IHcp. - by apply: cpcolor1U_correct => //; apply: IHcp. - by apply: cpcolor1K_correct => //; apply: IHcp. by apply: cpcolor1A_correct => //; apply: IHcp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)