proposition: Theorem Kempe_treeP cp et : size et = (cprsize cp).-1 -> reflect (Kempe_coclosure (ring_trace (rot 1 (cpring (cpmap cp)))) (ctrace et)) (~~ ctree_mem (Kempe_tree cp) (etrace et)).
proof: Proof. set Pcol := ring_trace _; rewrite /Kempe_tree. move: (cpcolor cp) (ctree_mem_cpcolor cp) => ctr Dctr. case Dh: (cprsize cp) => [|[|h]]. - by rewrite -size_ring_cpmap head_cpring in Dh. - by case: et => // _; left=> P1 closedP1 /closedP1[_ [[] ]]. set ctu := ctree_init_tree _; set gtu := gtree_init_tree _. have [] := @Kempe_tree_closure_correct h Pcol h.+2 ctu ctr gtu. apply: (Kempe_valid_restrict _ (Kempe_valid_init _ _)) => et1 /Dctr. case=> even_et1 [k gt_k Det1]; split. by rewrite /Pcol /ctrace -rot1_cons Det1 -trace_rot -map_rot; exists k. rewrite [LHS](canRL succnK (congr1 size Det1)) size_trace size_map. by rewrite size_ring_cpmap Dh. case: (Kempe_tree_closure h _ _ _ gtu) => [ctu' [gtr gtu']] Pcol_valid Pcol_sz. apply: (Kempe_completeP Pcol_valid (Pcol_sz _ _)); rewrite addn0. apply: Kempe_complete_init => et1 [k col_k Det1]; apply/Dctr. rewrite even_etrace /etrace; set g := etrace_perm et1. split=> //; exists (g \o k); first exact: coloring_inj (@permc_inj g) col_k. rewrite map_comp trace_permt sumt_permt. by rewrite -[trace _](rotK 1) -trace_rot -map_rot -Det1 rotr1_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring cfmap) fourcolor(cfcolor dyck ctree initctree gtree initgtree) fourcolor(gtreerestrict ctreerestrict)