proposition: Lemma bintree_of_nil_Dyck : bintree_of_Dyck nil_Dyck = BinLeaf.
proof: Proof. rewrite /bintree_of_Dyck. by case: (bintree_of_Dyck_spec _) => [[|t1 t2] [Pf Uniq]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree