proposition: Lemma bintree_of_DyckK D : Dyck_of_bintree (bintree_of_Dyck D) = D.
proof: Proof. by rewrite /bintree_of_Dyck; case: (bintree_of_Dyck_spec _) => /= [t []]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree