Coq comes with other systems together with the basic proof assistant. First of all there is a large library of reusable theories. It allows the user to exploit quite a lot of mathematics, most notably the natural numbers and their theory. And there are tools to manage proofs. We have pretty printers for HTML, LaTeX and even for natural languages. There are features for extensible syntax and facilities for searching in the library of mathematical theories. In addition, several user interfaces have been developed, so that we can use Coq almost on any machine with any operating system. Of course Coq is not the only proof assistant.

---