theorem :: ASYMPT_1:87

for k, n being Nat st k <= n holds
n choose k >= ((n + 1) choose k) / (n + 1) by Lm43;