Trouble with nat and int

Stream: new members

[Marc Masdeu]

Hi,

What is the one-liner that proves the following lemma?

variables {p : ℕ} [fact p.prime]
lemma euclid_int {a b : ℤ} : (p : ℤ) ∣ (a * b)  → (p : ℤ) ∣ a ∨ (p : ℤ) ∣ b :=
begin
    sorry
end

Definitely want to use nat.prime.dvd_mul, BTW. I tried push_cast, norm_cast, and all the _cast family that I could think of, with no luck... Thanks!

[Reid Barton]

docs#int.prime.dvd_mul'

[Marc Masdeu]

Oops sorry! Had overlooked that one...