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