Invariant checking of NRA transition systems via incremental reduction to LRA with EUF