proposition: Lemma enum_bintreeszP n : all (fun t => size_tree t == n) (enum_bintreesz n).
proof: Proof. by apply/allP => /= t /size_mem_enum_bintreeszP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype