for k being Nat ex N being Nat st
for x being Nat st N <= x holds
1 / (2 to_power x) < 1 / (x to_power k)