for i, n being Nat holds NEG_MOD (i,n) is_expressible_by n by NAT_D:1, POWER:34;