β : Type ?u.61783
A : Type ?u.61786
G : Type ?u.61789
M : Type u_1
R : Type ?u.61795
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 : x ≤ 1
n : ℕ
⊢ x * x ^ n ≤ 1
β : Type ?u.61783
A : Type ?u.61786
G : Type ?u.61789
M : Type u_1
R : Type ?u.61795
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 : x ≤ 1
n : ℕ
⊢ x ^ (n + 1) ≤ 1
rw [pow_succ]
no goals
β : Type ?u.61783
A : Type ?u.61786
G : Type ?u.61789
M : Type u_1
R : Type ?u.61795
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 : x ≤ 1
n : ℕ
⊢ x * x ^ n ≤ 1
exact Right.mul_le_one hx <| Right.pow_le_one_of_le hx