β : Type ?u.223542
A : Type ?u.223545
G : Type ?u.223548
M : Type ?u.223551
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n
β : Type ?u.223542
A : Type ?u.223545
G : Type ?u.223548
M : Type ?u.223551
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a ^ (n + 1)
rw [pow_succ]
no goals
β : Type ?u.223542
A : Type ?u.223545
G : Type ?u.223548
M : Type ?u.223551
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n
exact one_lt_mul_of_lt_of_le ha (one_le_pow_of_one_le ha.le _)