theorem :: NAT_D:51

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