This paper describes the actual implementation in the rewrite rule laboratory REVE, of an elementary procedure that checks inequalities between polynomials and is used for proving termination of rewriting systems, especially in the more difficult case of associative-commutative rewriting systems, for which a complete characterization is given.