proposition: Lemma enum_bintreesz_leqE n m : n <= m -> enum_bintreesz n = nth [::] (enum_bintreesz_leq m) n.
proof: Proof. move=> H; rewrite /enum_bintreesz. rewrite -nth_last size_enum_bintreesz /=. apply: enum_bintreesz_leq_leqE. by rewrite leqnn H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype