α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
⊢ a ^ m ≤ a ^ n
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
⊢ a ^ m ≤ a ^ n
have ha₀ : 0 < a := one_pos.trans_le ha
case intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
k : ℕ
hk : ↑k = n - m
⊢ a ^ m ≤ a ^ n
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
⊢ a ^ m ≤ a ^ n
lift n - m to ℕ using sub_nonneg.2 h with k hk
no goals
case intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
k : ℕ
hk : ↑k = n - m
⊢ a ^ m ≤ a ^ n
calc
  a ^ m = a ^ m * 1 := (mul_one _).symm
  _ ≤ a ^ m * a ^ k :=
    mul_le_mul_of_nonneg_left (one_le_pow_of_one_le ha _) (zpow_nonneg ha₀.le _)
  _ = a ^ n := by rw [← zpow_ofNat, ← zpow_add₀ ha₀.ne', hk, add_sub_cancel'_right]
no goals
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
k : ℕ
hk : ↑k = n - m
⊢ a ^ m * a ^ k = a ^ n
rw [← zpow_ofNat, ← zpow_add₀ ha₀.ne', hk, add_sub_cancel'_right]