Inequalities for binomial coefficients #
This file proves exponential bounds on binomial coefficients. We might want to add here the
bounds n^r/r^r ≤ n.choose r ≤ e^r n^r/r^r
in the future.
Main declarations #
nat.choose_le_pow
:n.choose r ≤ n^r / r!
nat.pow_le_choose
:(n + 1 - r)^r / r! ≤ n.choose r
. Beware of the fishy ℕ-subtraction.