\section{Bool}\label{Bool}

The BOOL library includes the following files:

\begin{itemize}

\item {\tt Bool.v} defines standard operations on booleans and states
  and proves simple facts on them.
\item {\tt IfProp.v} defines a disjunction which contains its proof
  and states its properties.
\item {\tt Zerob.v} defines the test against 0 on natural numbers and
  states and proves properties of it.
\item {\tt Orb.v} states and proves facts on the boolean or.
\item {\tt DecBool.v} defines a conditional from a proof of
  decidability and states its properties.
\end{itemize}