for k, n being natural Number holds
( k < k + n iff 1 <= n )