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