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