proposition: Lemma Kempe_complete_init ctr : (forall et, P (ctrace et) -> ctree_mem ctr (etrace et)) -> let ctu := ctree_init_tree h.+1 in let gtu := gtree_init_tree h.+1 in forall gtr, Kempe_complete (3 ^ h.+2) ctu ctr gtr gtu.
proof: Proof. move=> Pctr; split=> [|et norm [/Pctr | [e /negP init'e]]]; try by left. left; apply: (@leq_ltn_trans (3 ^ h.+1)); last by rewrite ltn_exp2l. by apply: ctree_max_size_proper; apply: ctree_init_tree_proper. right; apply: contraNeq init'e => /match_countP[w]. rewrite gtree_mem_init_tree => /andP[sz_w bal_w] etMw. rewrite /ctree_mem ctree_sub_init_tree !size_map -(matchpg_size etMw) sz_w. rewrite -matchg_pg // {}/norm in etMw *; set pre := permt _. rewrite !ctrace_permt !memc0_permt (matchg_memc0 etMw). have -> /=: even_trace (pre (etrace et)). apply: etrans (even_etrace et); rewrite /even_trace /ttail proper_permt. case: (etrace et) => [|[] ett] //=; rewrite /permt -map_comp; by apply: (congr1 even_tail (eq_map _ _)); case e => [] []. rewrite -[n in dyck n]odd_double_half -lt0n. have -> et': odd (count_cbit1 et') = cbit1 (sumt et'). by elim: et' => //= c et' IHet'; rewrite oddD IHet' cbit1_addc; case c. by rewrite !sumt_permt sumt_ctrace !permc0 even_dyck_pos. 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)