:: deftheorem defines NEG_MOD IDEA_1:def 6 :
for n, i being Nat holds NEG_MOD (i,n) = (NEG_N (i,n)) mod (2 to_power n);