for n being non zero Nat holds
( n - 1 is Nat & 1 <= n )