Termination is an important property of programs; notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting. Over the years many methods and tools have been developed to address the problem of deciding termination for specific problems (since it is undecidable in general). Ensuring reliability of those tools is therefore an important issue.

In this paper we present a library formalizing important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.

The sources are freely available at http://color.inria.fr/.