no goals
β : Type ?u.226813
A : Type ?u.226816
G : Type ?u.226819
M : Type ?u.226822
R : Type u_1
inst✝ : StrictOrderedSemiring R
a x y : R
n✝ m : ℕ
h : 1 < a
this : 0 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)
simpa only [one_mul, pow_succ] using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le