case zero
a : ℤ
⊢ ↑↑a = a % ↑Nat.zero

case succ
a : ℤ
n✝ : ℕ
⊢ ↑↑a = a % ↑(Nat.succ n✝)
n : ℕ
a : ℤ
⊢ ↑↑a = a % ↑n
cases n
case zero
a : ℤ
⊢ ↑a = a
case zero
a : ℤ
⊢ ↑↑a = a % ↑Nat.zero
rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]
no goals
case zero
a : ℤ
⊢ ↑a = a
rfl
case succ
a : ℤ
n✝ : ℕ
⊢ ↑↑a =
    ↑((match (motive := (x : ℕ) → ZMod x → ℕ) Nat.succ n✝ with
        | 0 => Int.natAbs
        | Nat.succ n => Fin.val)
        ↑a)
case succ
a : ℤ
n✝ : ℕ
⊢ ↑↑a = a % ↑(Nat.succ n✝)
rw [← val_int_cast, val]
no goals
case succ
a : ℤ
n✝ : ℕ
⊢ ↑↑a =
    ↑((match (motive := (x : ℕ) → ZMod x → ℕ) Nat.succ n✝ with
        | 0 => Int.natAbs
        | Nat.succ n => Fin.val)
        ↑a)
rfl