for n being Nat holds 2 |^ (n + 1) < (2 |^ (n + 2)) - 1