no goals
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Fintype G
n : ℤ
⊢ x ^ n = x ^ (n % ↑(Fintype.card G))
rw [zpow_eq_mod_orderOf, ← Int.emod_emod_of_dvd n (Int.coe_nat_dvd.2 orderOf_dvd_card_univ), ←
  zpow_eq_mod_orderOf]