fact: Fixpoint cfcbr1 (et : colseq) : ctree := if et is e :: et' then match g e with | Color0 => CtreeEmpty | Color1 => ctree_cons1 (cfcbr1 et') | Color2 => ctree_cons2 (cfcbr2 (ctree_cons_perm g) et') | Color3 => ctree_cons2 (cfcbr2 (ctree_cons_perm (Eperm132 \o g)) et') end else ctree_simple_leaf.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)