theorem Th11: :: IDEA_1:11

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