simpa [ZMod.nat_cast_val, ZMod.cast_id'] using h
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
a b : ZMod (Fintype.card G)
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b
no goals