Latvian National Olympiad 2025 Grade 12 Problem 4

Prime numbers $p$ and $q$ are such that $p^2 + pq + q^2$ is a square of some positive integer. Prove that $p^2 - pq + q^2$ is a prime number.

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Data.Nat.Prime.Defs

theorem solution (p q : ℕ) (hp : p.Prime) (hq : q.Prime)
    (h : ∃ a, p ^ 2 + p * q + q ^ 2 = a ^ 2) : (p ^ 2 + q ^ 2 - p * q).Prime := sorry

Login to submit a solution.