theorem Th121: :: GROUP_24:1

for a, b being Nat st a < b & b <> 0 holds
(2 * a) div b < 2