theorem Th8: :: NAT_2:8

for i, j being Nat st i >= j holds
j -' i = 0