proposition: Lemma cpcolor1R_correct n f : (forall k', coloring k' -> @cp_extcol cp1 (CpR n :: cp2) f k') -> cp_extcol (CpR n :: cp1) (cpcolor1 (CpR n) f) k.
proof: Proof. by case/(_ k col_k); rewrite cpring_ecpR map_rot trace_rot. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)