How to use negative numbers?

Stream: new members

[tsuki hao]

import Mathlib
import LeanCopilot

open Nat
open Finset
open BigOperators

example {m n k : ℕ} (hm : 1 < m) :
∑ k in range (n + 1), (choose (n + 1) k) * (-1) ^ k / (k + 1) ^ m = 1 / ((n + m) * (m - 1)!) := by
  sorry

What can I do to make the -1work?Maybe I should open some space?

[Yaël Dillies]

Replace (-1) by (-1 : ℤ)

[Kevin Buzzard]

You might want to consider removing the m-1 completely by replacing the variable m with m'+1 everywhere

[Kevin Buzzard]

If you do this then every occurrence of n will be of the form n+1 and you might then ask whether the equation is still true for n=-1. If it is then you'd be better off replacing n with n'-1 and proving the more general statement