theorem :: NAT_D:44

for i1, i2 being natural Number st i1 <= i2 holds
i1 -' 1 <= i2