theorem Th1: :: COMPLEX2:1

for a, b being Real st b > 0 holds
ex r being Real st
( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b )