\section{Relations}\label{Relations}

This library develops closure properties of relations.

\begin{itemize}
\item {\tt Relation\_Definitions.v} deals with the general notions
  about binary relations (orders, equivalences, ...)

\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
  closures of relations (by symmetry, by transitivity, ...) and
  lexicographic orderings.

\item {\tt Operators\_Properties.v} states and proves facts on the
  various closures of a relation.

\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
    Relation\_Operators.v} and \\
    {\tt Operators\_Properties.v} together.

\item {\tt Newman.v} proves Newman's lemma on noetherian and locally
  confluent relations.

\end{itemize}