for n being Nat st n >= 1 holds
n block 2 = (1 / 2) * ((2 |^ n) - 2)