Square roots in quadratic complexifications

Every element of QuadraticAlgebra R (-1) 0 is a square when R is an ordered field whose nonnegative elements are squares. The algebraic formula uses two nonnegative square roots in R, without completeness or an Archimedean assumption.

theorem QuadraticAlgebra.isSquare_of_forall_nonneg_isSquare {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (z : QuadraticAlgebra R (-1) 0) (hsq : ∀ {a : R}, 0 ≤ a → IsSquare a) : IsSquare z

Every element of R[i] is a square if every nonnegative element of R is a square.