apply isCoprime_of_prime_dvd
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ IsCoprime (u + v) (2 * v)
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ ¬(u + v = 0 ∧ 2 * v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u + v → ¬z ∣ 2 * v