exact even_iff_two_dvd.1 (Int.even_mul_succ_self n)
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)
no goals