Theorem: pow_le_real (HOLFloat/Float_theorem.lean)

State before:
a x : ℝ
ha1 : a ≠ 1
hx0 : x ≠ 0
ha0 : ¬a ≤ 0
hal1 : a < 1
k : ℕ
hk : (abs x)⁻¹ < a⁻¹ ^ k
⊢ (abs x)⁻¹ < (a ^ k)⁻¹
Tactic:
simpa using hk
State after:
no goals

State before:
a x : ℝ
ha1 : a ≠ 1
hx0 : x ≠ 0
ha0 : ¬a ≤ 0
hal1 : ¬a < 1
k : ℕ
hk : (abs x)⁻¹ < a ^ k
⊢ (abs x)⁻¹ < (a ^ (-↑k))⁻¹
Tactic:
simpa
State after:
no goals