no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]