Building the reals out of lambda calculus would be cool. I don't think however that your definition of mult_real is correct. For example if a=b=10 and eps=2, th

Building the reals out of lambda calculus would be cool. I don't think however that your definition of mult_real is correct. For example if a=b=10 and eps=2, then a(eps/2) x b(eps/2) could be anything between 9x9=81 and 11x11=121, whereas you'd want it to be between 99 and 101? How to fix this?