apply Int.dvd_mul_cancel_prime' notdvd_3_3 hkdvdright Int.prime_three
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ v
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 3 * v