proposition: Lemma enum_bintreesz_leq_leqE i n m : i <= n <= m -> nth [::] (enum_bintreesz_leq n) i = nth [::] (enum_bintreesz_leq m) i.
proof: Proof. move=> /andP[Hi Hn]; rewrite -(subnK Hn). elim: (m - n) => {m Hn} [| m ->] //. rewrite addSn /= nth_rcons size_enum_bintreesz ltnS (leq_trans Hi _) //. exact: leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype