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