1
\section{Relations}\label{Relations}
3
This library develops closure properties of relations.
6
\item {\tt Relation\_Definitions.v} deals with the general notions
7
about binary relations (orders, equivalences, ...)
9
\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
10
closures of relations (by symmetry, by transitivity, ...) and
11
lexicographic orderings.
13
\item {\tt Operators\_Properties.v} states and proves facts on the
14
various closures of a relation.
16
\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
17
Relation\_Operators.v} and \\
18
{\tt Operators\_Properties.v} together.
20
\item {\tt Newman.v} proves Newman's lemma on noetherian and locally