no goals
ι : Type ?u.128272
α : Type u_1
β : Type ?u.128278
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ < (a ^ m)⁻¹
convert one_div_pow_lt_one_div_pow_of_lt a1 mn using 1 <;> simp