English
For a prime p and x ∈ Nat, there exist a,b ∈ Nat with a ≤ p/2, b ≤ p/2 such that a^2 + b^2 ≡ x (mod p).
Русский
Для простого p и x ∈ Nat существуют a,b ∈ Nat с ограничениями a ≤ p/2, b ≤ p/2 и a^2 + b^2 ≡ x (mod p).
LaTeX
$$$\\exists a,b \\in \\mathbb{N},\\ a \\le \\frac{p}{2} \\land b \\le \\frac{p}{2} \\land a^2 + b^2 \\equiv x \\pmod p$$$
Lean4
/-- If `p` is a prime natural number and `x` is a natural number, then there exist natural numbers
`a ≤ p / 2` and `b ≤ p / 2` such that `a ^ 2 + b ^ 2 ≡ x [MOD p]`. This is a version of
`ZMod.sq_add_sq` with estimates on `a` and `b`. -/
theorem sq_add_sq_modEq (p : ℕ) [Fact p.Prime] (x : ℕ) : ∃ a b : ℕ, a ≤ p / 2 ∧ b ≤ p / 2 ∧ a ^ 2 + b ^ 2 ≡ x [MOD p] :=
by simpa only [← Int.natCast_modEq_iff] using Nat.sq_add_sq_zmodEq p x
