proposition: Lemma Kempe_valid_init : let ctu := ctree_init_tree h.+1 in let gtu := gtree_init_tree h.+1 in Kempe_valid ctu CtreeEmpty GtreeEmpty gtu.
proof: Proof. move: (ctree_init_tree_proper h.+1) (ctree_sub_init_tree h.+1). move: (ctree_init_tree _) => ctu ctu_ok Dctu. move: (gtree_init_tree _) (gtree_mem_init_tree h.+1) => gtu Dgtu. split=> // [|[]//|w|w]; rewrite ?Dgtu //; split=> // et. rewrite Dctu andbA andbC; case: (even_trace et) => //=. by rewrite -match_count_balanced -(match_count_eq Dgtu) gtree_sub_empty. 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)