for n being Nat holds
( n is even iff n mod 2 = 0 )