theorem :: INT_5:43

for p being Prime st p > 2 & ( p mod 8 = 1 or p mod 8 = 7 ) holds
2 is_quadratic_residue_mod p