proposition: Lemma ctree_leaf_table_size h : size (ctree_leaf_table h) = h.+1.
proof: Proof. rewrite /ctree_leaf_table_from /=; congr _.+1. rewrite -(odd_double_half h) addnC; move: (CtreeLeaf CtreeEmpty) 0. by elim: h./2 => [|h2 IHh] t n; [case: (odd h) | rewrite /= IHh]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree dyck)