Computer validated proofs of a toolset for adaptable arithmetic - Sylvie Boldo; Marc Daumas; Claire Moreau-Finot; Laurent Théry (CoRR, 2001)