β : Type ?u.56986
A : Type ?u.56989
G : Type ?u.56992
M : Type u_1
R : Type ?u.56998
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x * x ^ n
β : Type ?u.56986
A : Type ?u.56989
G : Type ?u.56992
M : Type u_1
R : Type ?u.56998
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)
rw [pow_succ]
no goals
β : Type ?u.56986
A : Type ?u.56989
G : Type ?u.56992
M : Type u_1
R : Type ?u.56998
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x * x ^ n
exact Right.one_le_mul hx <| Right.one_le_pow_of_le hx