theorem :: MOEBIUS2:1

for n, i being Nat st n >= 2 |^ ((2 * i) + 2) holds
n / 2 >= (2 |^ i) * (sqrt n)