Square Add 5 Square

Let $S$ be a set of natural numbers of the form $a ^ 2 + 5 b ^ 2$, where $a$ and $b$ are coprime positive natural numbers. Let $p \equiv 3 \pmod{4}$ be a prime dividing some element of $S$. Show that $2p$ is an element of $S$.

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

import Mathlib.Data.Nat.Prime.Defs

def S : Set ℕ := { n | ∃ a b : ℕ, a > 0 ∧ b > 0 ∧ a.Coprime b ∧ n = a ^ 2 + 5 * b ^ 2 }

theorem solution (p : ℕ) (hp : Nat.Prime p) (hpmod : p % 4 = 3) (hsp : ∃ n ∈ S, p ∣ n) :
    2 * p ∈ S := sorry

Login to submit a solution.