theorem :: PEPIN:16

for n being Nat st n is even holds
n + 1 is odd ;