for k, n being natural Number st k <= n holds
n - k is Element of NAT