a b : ℤ
⊢ Associated (natAbs a) (natAbs b) ↔ natAbs a = natAbs b
a b : ℤ
⊢ Associated a b ↔ natAbs a = natAbs b
rw [← dvd_dvd_iff_associated, ← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs,
  dvd_dvd_iff_associated]
no goals
a b : ℤ
⊢ Associated (natAbs a) (natAbs b) ↔ natAbs a = natAbs b
exact associated_iff_eq