adds general facts in the Reals library, whose need was detected in
experiments about computing PI