proposition: Lemma ctree_add_dyck_leaf_of m n d : ctree_add_dyck m n (ctree_leaf_of d) = ctree_leaf_of (gen_dyck m.+1 (m + n.*2) + d).
proof: Proof. elim: n m d => [|n IHn] m /=; first by rewrite addn0 gen_dyck_all_close. elim: m => [|m IHm] d; rewrite doubleS /=; first by rewrite addn0 IHn. by rewrite IHm IHn doubleS addnA -addnE !addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree dyck)