Dans cet article, nous proposons une tactique pour le système Coq qui, grâce à des outils algébriques tels que les bases de Gröbner et le théorème des zéros de Hilbert, et grâce à la tactique Ring, permet de montrer que des égalités dans un anneau commutatif en impliquent une autre.