Add algorithms for computational real operations
- addition, subtraction, division, square-root
- all functions are proved terminating
- Add an axiom to the standard library that logarithm is strictly increasing
- Add an axiom that square root is strictly monotonic and not only monotonic