β : Type ?u.218801
A : Type ?u.218804
G : Type ?u.218807
M : Type ?u.218810
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a * a ^ n
β : Type ?u.218801
A : Type ?u.218804
G : Type ?u.218807
M : Type ?u.218810
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)
rw [pow_succ]
no goals
β : Type ?u.218801
A : Type ?u.218804
G : Type ?u.218807
M : Type ?u.218810
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a * a ^ n
exact le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h