{ simp }
case h.ofNat.zero

⊢ (match Int.negOfNat Nat.zero with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑Nat.zero

case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)
case h.ofNat.succ
n_1 : ℕ
⊢ (match Int.negOfNat (Nat.succ n_1) with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑(Nat.succ n_1)