Sylvie Boldo, Catherine Lelay, Guillaume Melquiond: Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. CPP 2012: 289-304