Basic lemmas about the divisibility relation in ℤ.

theorem Int.coe_nat_dvd {m : ℕ} {n : ℕ} : ↑m ∣ ↑n ↔ m ∣ n

theorem Int.coe_nat_dvd_left {n : ℕ} {z : ℤ} : ↑n ∣ z ↔ n ∣ Int.natAbs z

theorem Int.coe_nat_dvd_right {n : ℕ} {z : ℤ} : z ∣ ↑n ↔ Int.natAbs z ∣ n