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

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