have bigger (n : ℕ) : 1 ≤ n + 1 := by
  simp only [le_add_iff_nonneg_left, zero_le]
case succ
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) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3
case succ
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
bigger : ∀ (n : ℕ), 1 ≤ n + 1
⊢ (n + 1) ^ 2 + 2 * (n + 1) * ∑ x in Finset.range (n + 1), x + S ^ 2 = (n + 1) ^ 3 + ∑ x in Finset.range (n + 1), x ^ 3