β : Type ?u.120218
A : Type ?u.120221
G : Type ?u.120224
M : Type u_1
R : Type ?u.120230
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n ≤ 1 ∧ 1 ≤ x ^ n ↔ x ≤ 1 ∧ 1 ≤ x
β : Type ?u.120218
A : Type ?u.120221
G : Type ?u.120224
M : Type u_1
R : Type ?u.120230
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n = 1 ↔ x = 1
simp only [le_antisymm_iff]
no goals
β : Type ?u.120218
A : Type ?u.120221
G : Type ?u.120224
M : Type u_1
R : Type ?u.120230
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x : M
n : ℕ
hn : n ≠ 0
⊢ x ^ n ≤ 1 ∧ 1 ≤ x ^ n ↔ x ≤ 1 ∧ 1 ≤ x
rw [pow_le_one_iff hn, one_le_pow_iff hn]