for a being Integer
for p being Prime st p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p holds
((a |^ ((p -' 1) div 2)) + 1) mod p = 0