Nonnegative norms in quadratic algebras

Over an ordered ring, a nonpositive discriminant makes the norm nonnegative (QuadraticAlgebra.norm_nonneg_of_discr_nonpos), as for ℚ(√d) with d < 0.

theorem QuadraticAlgebra.norm_nonneg_of_discr_nonpos {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} (h : discr a b ≤ 0) (z : QuadraticAlgebra R a b) : 0 ≤ norm z

The norm is nonnegative when the discriminant is nonpositive. Over an ordered ring, if b² + 4a ≤ 0 then every element of QuadraticAlgebra R a b has nonnegative norm.