for a, x being Integer
for p being Prime st a gcd p = 1 & ((x ^2) - a) mod p = 0 holds
x,p are_coprime