for i, j, k, l being Nat st i <= j & k <= j & i = (j -' k) + l holds
k = (j -' i) + l