for i, n, k, u being Nat st u > n |^ k & n >= k & k > i holds
(n choose i) * (u |^ i) < (u |^ k) / n