introduce and test finite_real assumption

TODO: rename real to extended_real (or similar)
and name finite_real to real.