theorem lemmonus: :: FIELD_9:1

for a, b being Nat st a <= b holds
a -' 1 <= b -' 1