for n being Nat holds n < (2 * n) + 1