for n being Nat holds not (n * n) + n,3 are_congruent_mod 5