no goals
ι : Type ?u.123201
α : Type u_1
β : Type ?u.123207
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_lt_one_div _ _).mpr (pow_lt_pow a1 mn) <;> exact pow_pos (zero_lt_one.trans a1) _