theorem :: PEPIN:22

for n being Nat holds
( 2 divides n iff n is even )