theorem FactorizationNoetherian.sum_of_two_squares_iff {n : ℕ} : (∃ (x : ℕ) (y : ℕ), n = x ^ 2 + y ^ 2) ↔ ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)