no goals
β : Type ?u.230037
A : Type ?u.230040
G : Type ?u.230043
M : Type ?u.230046
R : Type u_1
inst✝ : StrictOrderedSemiring R
a x y : R
n✝ m : ℕ
h₀ : 0 < a
h₁ : a < 1
n : ℕ
⊢ a ^ (n + 1) < a ^ n
simpa only [pow_succ, one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one