proposition: Lemma size_bintree_of_Dyck D : (size_tree (bintree_of_Dyck D)).*2 = size D.
proof: Proof. by rewrite -{2}(bintree_of_DyckK D) size_Dyck_of_bintree. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree