Nous décrivons une interface entre Coq et Maple. Il s'agit d'importer, dans Coq, les calculs fait par Maple sur les expressions algébriques dans un corps. Nous pouvons alors soit faire juste du calcul, qui ne requiert aucune validation, soit faire du calcul dans une preuve, qui devra être prouvé correct par Coq (approche sceptique). Ces preuves de correction sont complètement automatiques grâce à la tactique Field. Nous donnerons un aperçu de cette tactique qui prouve les égalités sur les corps et génère les conditions de bord nécessaires (non-nullité des dénominateurs) devant être montrées par l'utilisateur. Cette tactique est réflexive, ce qui assure à la fois efficacité et correction. Nous présenterons ensuite, par des exemples, l'interface dont l'implantation est particulièrement légère et simplement extensible à d'autres fonctions de Maple.