proposition: Lemma enum_bintreesz_countE n t : size_tree t == n -> count_mem t (enum_bintreesz n) = 1.
proof: Proof. move/mem_enum_bintreesz => H. by rewrite (count_uniq_mem _ (enum_bintreesz_uniq n)) H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype