proposition: Lemma Kempe_validP ctu ctr gtr gtu : Kempe_valid ctu ctr gtr gtu -> forall et, size et = h.+1 -> ~~ ctree_mem ctu (etrace et) -> Kempe_coclosure P (ctrace et).
proof: Proof. move=> [[_ Dctu] _ _ _ closedP] et0 sz_et0 ct'et0. pose et := ctrace (etrace et0) => P1 closedP1 P1et0. have{P1et0} P1et: P1 et by rewrite [et]ctrace_permt; case/closedP1: P1et0. have [_ [w0 etMw0 w0P1]] := closedP1 _ P1et. move: (take _ w0) (matchg_cgram etMw0) => w Dw0. have w0bal: gram_balanced 0 false w0. by have [_] := matchg_balanced etMw0; rewrite sumt_ctrace. have{etMw0} et0Mw: matchpg Bstack0 (etrace et0) w by rewrite -matchg_pg -Dw0. have [gt_w||et1 closedPet1 et1Mw] := closedP w. - case/negP: ct'et0; rewrite /ctree_mem Dctu even_etrace /= addn_eq0. by apply/nandP; right; apply/match_countP; exists w. - by apply/andP; rewrite (matchpg_size et0Mw) size_map sz_et0 -Dw0. by apply/closedPet1/w0P1; rewrite // Dw0 matchg_pg // -Dw0. 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)