proposition: Lemma ctree_leaf_table_sub h i b0 : i <= h -> let cet := [:: ccons (odd i) b0] in let n_i := i + count_cbit1 cet in ctree_table_sub (ctree_leaf_table h) i b0 = (if Color0 \in cet then CtreeEmpty else ctree_leaf_of (dyck n_i)).
proof: Proof. rewrite /ctree_leaf_table -{1 2 4}[i]odd_double_half. move: (odd i) i./2 => b1 m; rewrite (addnC b1) => lemh. rewrite /= cbit1_ccons inE addn0 -addnA -{2}[m]addn0. set t1 := CtreeLeaf _; rewrite -{1}[t1]/(ctree_leaf_of (dyck 0.*2)). rewrite -{t1}[t1]/(ctree_leaf_of (dyck 1.*2)). elim: m 0 h lemh => [|m IHm] n. by rewrite /= !add0n addnC; case: b1 b0 => [[] [|[]] | []]. case=> [|[|h]] // /(IHm n.+1); rewrite addSnnS => <-. by rewrite /dyck /= ctree_add_dyck_leaf_of !addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree dyck)