for p being Prime
for a being Element of (GF p) holds
( a is not_quadratic_residue iff Lege_p a = - 1 )