theorem NP0: :: NEWTON07:10

for n being odd Nat holds n choose ((n + 1) / 2) = n choose ((n - 1) / 2)