𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), x < 0 → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ (fun x => x ^ p / x ^ q) =ᶠ[atBot] fun x => x ^ (↑p - ↑q)
apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : x < 0
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), x < 0 → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
intro x hx
no goals
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : x < 0
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
simp [zpow_sub₀ hx.ne]