theorem MFR: :: NEWTON06:72

for a being non zero Nat
for b being Nat st b mod a < [/(a / 2)\] holds
frac (b / a) < 1 / 2