exact Int.dvd_mul_cancel_prime' hsubodd hkdvdleft Int.prime_two hkdvdright
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬2 ∣ u - v
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
no goals