for n being Nat st 1 < n holds
0. (Z/ n) = 0