unfold HSub.hSub
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m - ofNat (Nat.succ n)
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = instHSub.1 m (ofNat (Nat.succ n))