use N + 1
case ha.hl
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ ∃ a,
    ∀ b ≥ a,
      (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) b =
        (fun k =>
            (↑k ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) +
              s * ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
          b
case h
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ ∀ b ≥ N + 1,
    (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) b =
      (fun k =>
          (↑k ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) +
            s * ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
        b