for n, m being Nat
for k being Element of NAT st k <> 0 & k + m <= n holds
m < n