cases n with
| ofNat n => contradiction
| negSucc n =>
  simp only [abs]
  unfold HSub.hSub
  unfold instHSub
  unfold Sub.sub
  unfold Int.instSubInt
  unfold Int.sub
  simp only
  rw [neg_succ_eq_neg_ofNat_succ]
m n : Int
h : n < 0
⊢ m + n = m - ofNat (abs n)
no goals