for d being Integer ex n being non zero Nat st 2 to_power (n - 1) > d