theorem :: NEWTON07:67

for n being Nat holds ((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2) = ((n + 5) choose 2) - ((n + 5) choose 0)