fact: Fixpoint ctree_size (t : ctree) : nat := match t with | CtreeNode t1 t2 t3 => ctree_size t1 + (ctree_size t2 + ctree_size t3) | CtreeLeaf _ => 1 | CtreeEmpty => 0 end.
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)