\section{Binary integers : ZArith}
The {\tt ZArith} library deals with binary integers (those used
by the {\tt Omega} decision tactic).
Here are defined various arithmetical notions and their properties,
similar to those of {\tt Arith}.