for a, c being Nat
for b being non zero Nat st a * b < c & c < a * (b + 1) holds
( not a divides c & not c divides a )