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