proposition: Lemma Kempe_valid_restrict ctr ctu gtu gtr : (forall et, ctree_mem ctr et -> P (ctrace et) /\ size et = h.+1) -> Kempe_valid ctu CtreeEmpty gtr gtu -> Kempe_valid ctu ctr gtr gtu.
proof: Proof. move=> Dctr [[Hctu Ectu] ? Dgtr Dgtu closedP]; split=> // et ct_et. by case/Dctr: ct_et; split; first by exists (ctrace et). 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)