Peano Small example on defining inductive proofs, check out post below. https://wg-romank.github.io/peano/