proposition: Lemma mem_enum_bintreesz n t : size_tree t == n -> t \in enum_bintreesz n.
proof: Proof. elim/ltn_ind: n t => [[_|n IHn]] [|l r] //=. rewrite add1n addSn eqSS => /eqP Hn. rewrite enum_bintreeszE; apply/flattenP. exists [seq BinNode tl tr | tl <- enum_bintreesz (size_tree l), tr <- enum_bintreesz (n - (size_tree l))]; first last. apply/allpairsP; exists (l, r); split => //=. - by apply IHn => //; rewrite -Hn; apply leq_addr. - apply IHn => //; first exact: leq_subr. by rewrite -Hn addKn. apply/mapP; exists (size_tree l) => //. by rewrite mem_iota /= add0n ltnS -Hn leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype