theorem Lem1: :: BAGORD_2:2

for n, m being Nat holds m -' n >= m - n