proposition: Lemma size_enum_bintreeszE n : size (enum_bintreesz n) = Catalan_bin n.
proof: Proof. rewrite /Catalan_bin /enum_bintreesz -[LHS]last_map ; congr last. elim: n => //= n IHn. rewrite [LHS]/= map_rcons IHn /=; congr rcons. rewrite -[RHS]/(sumn (map _ (iota 0 n.+1))). rewrite -[LHS]/(size (flatten (map _ (iota 0 n.+1)))). rewrite size_flatten /shape -map_comp; congr sumn. apply eq_in_map => i; rewrite mem_iota /= add0n ltnS => Hi. rewrite size_allpairs -!IHn !(nth_map [::]) // size_enum_bintreesz ltnS //. exact: leq_subr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype