no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ y ^ (-(m + 1)) < x
rwa [zpow_neg, inv_lt (zpow_pos_of_pos hyp _) hx]
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-(m + 1) + 1)
rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv hx (zpow_pos_of_pos hyp _)]