for n being non zero square-free Nat
for a being non zero Nat st a divides n holds
a,n div a are_coprime