simp [Int.neg]
case h.ofNat
n : ℕ
⊢ Int.neg (Int.neg (Int.ofNat n)) = Int.ofNat n
case h.ofNat
n : ℕ
⊢ (match Int.negOfNat n with
    | Int.ofNat n => Int.negOfNat n
    | Int.negSucc n => ↑n + 1) =
    ↑n