simp_rw [div_eq_mul_inv, cpow_neg]
case h.e'_5
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(↑σ + ↑t * I + 1))
no goals