Nonnegative square roots of square elements

A square in a linearly ordered ring has a nonnegative square root, by taking the absolute value of any square root. Only compatibility of the order with addition is needed.

theorem IsSquare.exists_nonneg_sq {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedAddMonoid R] {a : R} (ha : IsSquare a) : ∃ (r : R), 0 ≤ r ∧ r ^ 2 = a

A square in a linearly ordered ring has a nonnegative square root.