proposition: Lemma Catalan_bin_leqE i m : i <= m -> nth 0 (Catalan_bin_leq m) i = Catalan_bin i.
proof: Proof. rewrite /Catalan_bin => Hi. rewrite -nth_last size_Catalan_bin_leq /= -(subnK Hi). elim: (m-i) => // d <-. by rewrite addSn nth_rcons size_Catalan_bin_leq ltnS leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype