The inverse of x is a prime field square iff x is.
Theorem: pfield-squarep-of-inv
(defthm pfield-squarep-of-inv (implies (and (dm::primep p) (fep x p)) (equal (pfield-squarep (inv x p) p) (pfield-squarep x p))))
