show _ + 1 = _
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
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ (i * i + i) / 2 + i + 1 =
    ((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