proposition: Theorem card_bintreesz n : #|bintreesz n| = Catalan_bin n.
proof: Proof. rewrite /= !cardT -!(size_map val) !enumT unlock /=. rewrite subType_seqP ?enum_bintreeszP //=. by rewrite size_enum_bintreeszE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype