theorem N2POWINPOLY: :: ASYMPT_2:16

for x being Nat st 1 < x holds
for N, c being Nat ex n being Nat st
( N <= n & not 2 to_power n <= c * (n to_power x) )