proposition: Lemma enum_bintreeszE n : enum_bintreesz n.+1 = flatten [seq [seq BinNode tl tr | tl <- enum_bintreesz i, tr <- enum_bintreesz (n - i)] | i <- iota 0 n.+1].
proof: Proof. rewrite [in LHS]/enum_bintreesz. rewrite -nth_last size_enum_bintreesz [n.+2.-1]/=. rewrite nth_rcons -!/(enum_bintreesz_leq _) !size_enum_bintreesz ltnn eq_refl. congr flatten; apply eq_in_map => i. rewrite mem_iota add0n ltnS /= => Hi. by rewrite -!(enum_bintreesz_leqE (m := n)) // leq_subr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype