rw [add_sub_cancel, mul_comm]
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 : ℤ
⊢ 2 ∣ (n + 1) * (n + 1 - 1)
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 : ℤ
⊢ 2 ∣ n * (n + 1)