m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ natAbs m ∨ p ∣ natAbs n
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ ↑p ∣ m ∨ ↑p ∣ n
rw [Int.coe_nat_dvd_left, Int.coe_nat_dvd_left]
no goals
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ natAbs m ∨ p ∣ natAbs n
exact Int.Prime.dvd_mul hp h