We can inductively define familiar operations like addition and multiplication.

There are several alternatives: we could induct on the second argument, on the first argument, or on both arguments: