fact: Definition Kempe_complete sz ctu ctr gtr gtu := [/\ ctree_size ctu < sz \/ ctr = CtreeEmpty /\ (forall w, ~ gtree_mem gtr w) & forall et, let norm_et e := permt (edge_rot e) (etrace et) in P (ctrace et) \/ (exists e, ~ ctree_mem ctu (norm_et e)) -> ctree_mem ctr (etrace et) \/ gtree_sub gtu Bstack0 et = 0].
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)