for h being non zero Nat
for q being Prime st not q,h are_coprime holds
q divides h