theorem NatOneLe: :: PRIMRECI:1

for k being Nat holds
( not k is zero iff 1 <= k )