theorem :: NAT_D:54

for k, i, j being natural Number st i <= j -' k & k <= j holds
i + k <= j