U. Berger and S. Lloyd, “A coinductive approach to verified exact real number computation”, ECEASST, vol. 23, Dec. 2009.