Inspiration: Another Test Problem from Kelly's Group.
Coq is an interactive proof assistant. What this means is that Coq helps you prove theorems in a way that can be mechanically checked by Coq itself. This technology could be used to prove mathematical theorems, or develop formally correct software.
A famous example of a notorious theorem whose formal proof was developed in Coq is the four color theorem (download the proof here). Also, it has been used to generate a formally correct C compiler, which is pretty cool, if you think about it.
Behold we prove in Coq as a teaser
We shall begin by defining the natural numbers along with
1 2 3 4 5 6
We then, define
1 2 3 4 5 6 7 8
Now, we can prove the theorem we desire.
1 2 3
And we are done!
Alternately, you could also use this: