for m being Nat
for t being Integer st m * t >= 1 holds
t >= 1