theorem N20: :: NEWTON07:9

for k, n being Nat holds (k + n) choose n = (k + n) choose k