theorem :: STIRL2_1:53

for n being Nat holds (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3)