theorem :: NUMBER15:79

for n being Nat holds
( not n is even or n, 0 are_congruent_mod 4 or n,2 are_congruent_mod 4 )