theorem Th5: :: IRRAT_1:5

for k, n being Nat holds n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k)