From Coinductive Proofs to Exact Real Arithmetic: Theory and Applications