no goals
ι : Type ?u.126922
α : Type u_1
β : Type ?u.126928
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_le_one_div_pow_of_le a1 mn using 1 <;> simp