Coq is a programming language and "proof assistant", where one can state and prove theorems which are checked for soundness by Coq itself. Looking at an example formalization of the hypernatural numbers, we'll explore what makes such a tool useful, interesting, and even fun! At the end of this talk attendees will hopefully have reasons to consider using Coq or similar tools themselves, and incidentally be able to construct a non-standard model of arithmetic (whenever the need arises).