Theorem: Section15sheet2.int_dvd_iff (FormalisingMathematics2024/Section15numberTheory/Sheet2.lean)

State before:
x n : ℤ
hn : n ≠ 0
⊢ x ∣ n ↔ Int.natAbs x ∈ Nat.divisors (Int.natAbs n)
Tactic:
simp [hn]
State after:
no goals