for i, n being Nat st i is_expressible_by n holds
ADD_MOD (i,(NEG_MOD (i,n)),n) = 0