proposition: Lemma size_mem_enum_bintreeszP n t : t \in enum_bintreesz n -> size_tree t = n.
proof: Proof. have [m] := ubnP n; elim: m => // m IHm in n t * => /ltnSE. case: n => [_|n ltnm]; first by rewrite enum_bintreesz0 inE => /eqP ->. rewrite enum_bintreeszE => /flatten_mapP[j]. rewrite mem_iota /= add0n ltnS => lejn. have ltjn1 := leq_ltn_trans lejn ltnm. have:= leq_subr j n; rewrite -ltnS => /leq_trans/(_ ltnm) ltnjn1. move/allpairsP => [[l r] /= [/(IHm _ _ ltjn1) szl /(IHm _ _ ltnjn1) szr ->{t}]]. by rewrite /= szl szr add1n addSn addnC subnK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype