Theorem: IMOSL.IMO2014A1.d_succ (IMOSLLean4/IMO2014/A1/A1.lean)

State before:
z : ℕ → ℤ
n : ℕ
⊢ d z (n + 1) = (range (n + 1)).sum z - ↑n * z (n + 1)
Tactic:
rw [d, sum_range_succ, Int.natCast_add, Int.natCast_one,
  add_one_mul (α := ℤ), add_sub_add_right_eq_sub]
State after:
no goals