for n being Nat
for a being non trivial Nat holds Px (a,n), Py (a,n) are_coprime