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.