Berger, U.; Lloyd, S. A Coinductive Approach to Verified Exact Real Number Computation. eceasst 2009, 23.