Central binomial coefficients #
This file proves properties of the central binomial coefficients (that is,
nat.choose (2 * n) n).
Main definition and results #
An exponential lower bound on the central binomial coefficient.
This bound is weaker than
four_pow_n_lt_n_mul_central_binom, but it is of historical interest
because it appears in Erdős's proof of Bertrand's postulate.