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