no goals
β : Type ?u.6110
A : Type ?u.6113
G : Type ?u.6116
M : Type u_1
R : Type ?u.6122
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
H : 1 ≤ a
⊢ 1 ≤ a ^ 0
simp
β : Type ?u.6110
A : Type ?u.6113
G : Type ?u.6116
M : Type u_1
R : Type ?u.6122
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
H : 1 ≤ a
k : ℕ
⊢ 1 ≤ a * a ^ k
β : Type ?u.6110
A : Type ?u.6113
G : Type ?u.6116
M : Type u_1
R : Type ?u.6122
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
H : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)
rw [pow_succ]
no goals
β : Type ?u.6110
A : Type ?u.6113
G : Type ?u.6116
M : Type u_1
R : Type ?u.6122
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
H : 1 ≤ a
k : ℕ
⊢ 1 ≤ a * a ^ k
exact one_le_mul H (one_le_pow_of_one_le' H k)