Check if a prime field element is a square.
This is more general than elliptic curve libraries, but it finds some uses in elliptic curves over prime fields (perhaps this should be moved to the prime field library). We non-constructively check whether there exists a square root in the prime field. The witness function returns a root, if one exists.
(defthm pfield-squarep-suff (implies (and (fep r p) (equal (mul r r p) x)) (pfield-squarep x p)))
(defthm booleanp-of-pfield-squarep (b* ((yes/no (pfield-squarep x p))) (booleanp yes/no)) :rule-classes :rewrite)