for p being Prime
for a being Element of (GF p) st a <> 0 holds
a |^ 2 is quadratic_residue by Th25;