apply huvcoprime.isUnit_of_dvd' <;>
  apply Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * u

case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * v