for n, k being Nat
for p being ExtReal st k <= (2 |^ n) * n & n <= p holds
k / (2 |^ n) <= p