theorem :: STIRL2_1:49
for n being Nat st n >= 3 holds
n block 4 = (1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4)