simp [
  Nat.add_assoc (i*i+i) i i, 
  Nat.add_div (a := i*i+i), 
  ←mul_two i,
  Nat.mul_div,
  not_two_le,
  Nat.add_assoc ((i * i + i) / 2 + i),
  Nat.dvd_iff_mod_eq_zero
]
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 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
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ 1 =
    (if Nat.succ (i * i + i + i * 2) % 2 = 0 then 1 else 0) +
      if Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = 0 then 1 else 0