for i, n being Nat st i is_expressible_by n holds
ADD_MOD (0,i,n) = i by NAT_D:24;