have haddodd : ¬Even (u + v) := by simp [huvodd, parity_simps]
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)