theorem :: INT_5:38

for p being Prime st p > 2 & p mod 4 = 3 holds
not - 1 is_quadratic_residue_mod p