theorem Th17: :: NUMBER03:17

for a, b, m being Integer st a < b holds
ex k being Nat st
( m < (((b - a) * k) + 1) - a & k = |.[/((((m + a) - 1) / (b - a)) + 1)\].| )