no goals
β : Type ?u.216636
A : Type ?u.216639
G : Type ?u.216642
M : Type ?u.216645
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n m : ℕ
H : 1 ≤ a
⊢ 1 ≤ a ^ 0
rw [pow_zero]
β : Type ?u.216636
A : Type ?u.216639
G : Type ?u.216642
M : Type ?u.216645
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
H : 1 ≤ a
n : ℕ
⊢ 1 ≤ a * a ^ n
β : Type ?u.216636
A : Type ?u.216639
G : Type ?u.216642
M : Type ?u.216645
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
H : 1 ≤ a
n : ℕ
⊢ 1 ≤ a ^ (n + 1)
rw [pow_succ]
no goals
β : Type ?u.216636
A : Type ?u.216639
G : Type ?u.216642
M : Type ?u.216645
R : Type u_1
inst✝ : OrderedSemiring R
a x y : R
n✝ m : ℕ
H : 1 ≤ a
n : ℕ
⊢ 1 ≤ a * a ^ n
simpa only [mul_one] using
  mul_le_mul H (one_le_pow_of_one_le H n) zero_le_one (le_trans zero_le_one H)