fact: Definition do_Birkhoff_check2 et ctu gtu chk := let ctr := ctree_of_ttail (etrace et) in if Color0 \in et then false else let: (ctu', GtreePair gtr gtu') := Kempe_tree_closure h.-1 h ctu ctr gtu in gtree_empty gtr && (check_basis ctu' || chk ctu' gtu').
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)