theorem Th35: :: NAT_D:35

for a, b being natural Number holds a -' b <= a