proposition: Lemma size_Dyck_of_bintree t : size (Dyck_of_bintree t) = (size_tree t).*2.
proof: Proof. elim: t => //= l Hl r Hr. by rewrite size_cat /= {}Hl Hr addnS -doubleD -doubleS -addnA add1n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree