proposition: Lemma gcol_perm : coloring k0 /\ cp_tr0 k0 -> forall c (h : edge_perm), let k x := c +c h (k0 x) in coloring k /\ cp_tr0 k.
proof: Proof. move=> [k0col tr_k0] c h k; split. suffices inj_ch: injective (addc c \o h) by apply: coloring_inj inj_ch k0col. by apply: inj_comp; [apply: addcI | apply: permc_inj]. rewrite /cp_tr0 /eptrace (map_comp (addc c)) (map_comp h). by rewrite -2!map_rot ptrace_addc -/(permt h) ptrace_permt etail_permt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)