Description: Equivalent to saying that the square of the imaginary component of the square root of a complex number is a nonnegative real number. Lemma for sqrtcval . See imsqrtval . (Contributed by RP, 11-May-2024)