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