a b : ℤ
⊢ natAbs a = natAbs b ↔ a = b ∨ a = -b
a b : ℤ
⊢ Associated a b ↔ a = b ∨ a = -b
rw [Int.associated_iff_natAbs]
no goals
a b : ℤ
⊢ natAbs a = natAbs b ↔ a = b ∨ a = -b
exact Int.natAbs_eq_natAbs_iff