Coinductive Formal Reasoning in Exact Real Arithmetic (Logical Methods in Computer Science, 2008)