for a, x being Nat
for p being Prime st a,p are_coprime & a,x * x are_congruent_mod p holds
x,p are_coprime