apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) / 2 = ∑ i ∈ range (n + 1), i
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) = 2 * ∑ i ∈ range (n + 1), i