case zero
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast

case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast
cases n
case succ.h
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
x✝ : ZMod (Nat.succ n✝)
⊢ (Int.cast ∘ cast) x✝ = ↑x✝
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast
ext
no goals
case succ.h
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
x✝ : ZMod (Nat.succ n✝)
⊢ (Int.cast ∘ cast) x✝ = ↑x✝
simp [ZMod, ZMod.cast]