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

State before:
z : ℕ → ℤ
⊢ d z 1 = z 0
Tactic:
rw [d_succ, sum_range_one, Nat.cast_zero, zero_mul, sub_zero]
State after:
no goals