no goals
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ natAbs a = natAbs b ↔ a = b
simpa only [Int.natAbs_neg, neg_inj] using
  natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) (neg_nonneg_of_nonpos hb)