theorem AMB: :: NEWTON05:11

for a, b being Nat holds a mod b <= a