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