for n, m being Nat st m = [\(n / 2)/] & n >= 2 holds
n choose m >= (2 |^ n) / n