exact Int.mod_modEq _ _
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ i % ↑(orderOf x) ≡ i [ZMOD ↑(orderOf x)]
no goals