English
In a linearly ordered semiring with appropriate additive properties, sums of squares are nonnegative.
Русский
В упорядоченном по линейному порядку полусистеме суммы квадратов неотрицательны.
LaTeX
$$$\forall R [\text{Semiring } R] [\text{LinearOrder } R] [\text{IsStrictOrderedRing } R] [\ExistsAddOfLE R],\; IsSumSq(s) \Rightarrow 0 \le s$$$
Lean4
/-- In a linearly ordered semiring with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`),
sums of squares are non-negative.
-/
theorem nonneg {R : Type*} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {s : R}
(hs : IsSumSq s) : 0 ≤ s := by
induction hs using IsSumSq.rec' with
| zero => simp
| sq_add hx _ h => exact add_nonneg (IsSquare.nonneg hx) h
