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