theorem int.not_prime_of_int_mul {a b : ℤ} {c : ℕ} (ha : 1 < a.nat_abs) (hb : 1 < b.nat_abs) (hc : a * b = ↑c) :