simp [sum]
case succ
n : ℕ
ih : ↑(sum n) = ↑n * (↑n + 1) / 2
⊢ ↑(sum (Nat.succ n)) = ↑(Nat.succ n) * (↑(Nat.succ n) + 1) / 2
case succ
n : ℕ
ih : ↑(sum n) = ↑n * (↑n + 1) / 2
⊢ ↑n + 1 + ↑(sum n) = (↑n + 1) * (↑n + 1 + 1) / 2