theorem :: PEPIN:43

for n being Nat st n <> 0 holds
- n < n ;