simp [h, h2, zpow_add, zpow_mul]
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
h2 : x ^ m = x ^ (↑n * (m / ↑n) + m % ↑n)
⊢ x ^ m = x ^ (m % ↑n)
no goals