Lemmas about Nat.Prime using Ints

ink

theorem Int.not_prime_of_int_mul {a : ℤ} {b : ℤ} {c : ℕ} (ha : 1 < Int.natAbs a) (hb : 1 < Int.natAbs b) (hc : a * b = ↑c) : ¬Nat.Prime c

ink

theorem Int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : Nat.Prime p) {m : ℤ} {n : ℤ} {k : ℕ} {l : ℕ} (hpm : ↑(p ^ k) ∣ m) (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k + l + 1)) ∣ m * n) : ↑(p ^ (k + 1)) ∣ m ∨ ↑(p ^ (l + 1)) ∣ n

ink

theorem Int.Prime.dvd_natAbs_of_coe_dvd_sq {p : ℕ} (hp : Nat.Prime p) (k : ℤ) (h : ↑p ∣ k ^ 2) : p ∣ Int.natAbs k