Note: To follow along with this post create a new Lean file and write the following at the top of your Lean file. If you do not have a copy of Lean installed you can follow along here (but it will run slower). In this post we will consider the type of natural numbers \(\mathbb{N} […]