no goals
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
⊢ orderOf (x ^ n) ∣ orderOf x
rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]