for n being Nat holds
not not n mod 5 = 0 & ... & not n mod 5 = 4