exact ⟨haddcoprime.symm, hsubcoprime.symm, haddsubcoprime.symm⟩
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
haddsubcoprime : IsCoprime (u + v) (u - v)
⊢ IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)
no goals