for i being Nat st 1 < i holds
0 < i -' 1