no goals
ι : Type ?u.121089
α : Type u_1
β : Type ?u.121095
inst✝ : LinearOrderedSemifield α
a b c d e : α
m✝ n✝ : ℤ
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m
refine' (one_div_le_one_div _ _).mpr (pow_le_pow a1 mn) <;>
  exact pow_pos (zero_lt_one.trans_le a1) _