have : (N ^ (-σ) - t ^ (-σ)) / σ ≤ N ^ (-σ) / σ :=
  div_le_div_right σpos |>.mpr (by simp [Real.rpow_nonneg (by linarith)])
case h
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ
case h
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ