unfold Sub.sub
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => Sub.sub a b }.1 m (ofNat (Nat.succ n))
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => instSubInt.1 a b }.1 m (ofNat (Nat.succ n))