proposition: Lemma enum_bintreesz_uniq n : uniq (enum_bintreesz n).
proof: Proof. elim/ltn_ind: n => [[// | n IHn]]. rewrite enum_bintreeszE. have [i] := ubnPgeq n.+1; elim: i => // i IHi /ltnSE-ltin. rewrite -addn1 iotaD add0n /=. rewrite map_cat flatten_cat /= cats0 cat_uniq. rewrite {}IHi /=; last exact: (leq_trans ltin). apply/andP; split. - apply/hasP => [] /= [[| l r]] /allpairsP/= [[l1 r1] /= []]. + by move=> _ _ /eqP; rewrite eqE. + move/size_mem_enum_bintreeszP => Hszl1 _ -> {l r}. move/flattenP => [/= ltj /mapP /= [j]]. rewrite mem_iota /= add0n => Hj ->. move/allpairsP => [/= [l r] /= []]. move/size_mem_enum_bintreeszP => Hszl _ [] Hl1 _. move: Hszl1 Hj; rewrite Hl1 Hszl => ->. by rewrite ltnn. - have:= IHn i ltin. elim: (enum_bintreesz i) => [// | l ll IHll] /= /andP[Hnotin {}/IHll Hrec]. rewrite cat_uniq Hrec /= andbT. apply/andP; split. + rewrite map_inj_uniq; first by apply IHn; apply leq_subr. by move=> r1 r2 []. + apply/hasP => [] /= [t]. move/allpairsP => [] /= [l1 r1 /= [Hl1 _ ->{t}]]. move/mapP => [] /= r2 _ [] Heql _. by move: Hnotin; rewrite -Heql Hl1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype