conv => rw [div_eq_mul_inv, ← one_div]; rhs; rw [← one_mul |x ^ (s.re + 1)|⁻¹]
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 2⁻¹ - x| / |x ^ (s.re + 1)| ≤ |x ^ (s.re + 1)|⁻¹
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (s.re + 1)|⁻¹ ≤ 1 * |x ^ (s.re + 1)|⁻¹