no goals
a✝ b✝ : ℤ
n : ℕ
a : ℤ
x✝ : a ∈ Iic 0
b : ℤ
hb : b ∈ Iic 0
hab : a < b
⊢ natAbs b < natAbs a
simpa [Int.natAbs_neg] using
  natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)