a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ ↑(natAbs a) < ↑(natAbs b)
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ a * a < b * b
rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]
no goals
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ ↑(natAbs a) < ↑(natAbs b)
exact Int.ofNat_lt.symm