simp only [le_add_iff_nonneg_left, zero_le]
n✝ : ℕ
ih : (∑ x in Finset.range (n✝ + 1), x) ^ 2 = ∑ x in Finset.range (n✝ + 1), x ^ 3
S : ℕ := ∑ x in Finset.range (n✝ + 1), x
hS : S = ∑ x in Finset.range (n✝ + 1), x
n : ℕ
⊢ 1 ≤ n + 1
no goals