simp only [sum_succ, ih, Nat.add_succ, add_zero, Nat.succ_mul, Nat.mul_succ, Nat.succ_div, 
  Nat.isUnit_iff]
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ sum (fun n => n) (Nat.succ i) = Nat.succ i * (Nat.succ i + 1) / 2
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ Nat.succ ((i * i + i) / 2 + i) =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0