for r, u being Real st r > 0 & u > 0 holds
ex k being Nat st u / (2 |^ k) <= r