theorem :: NEWTON07:68

for n being Nat holds (((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2)) + ((n + 6) choose 3) = ((n + 7) choose 3) - ((n + 6) choose 1)