Be sure
Nat_as the type and notNat
It seems unnecessary to use a package manager like lake, but it was the only way
I could get the imports to work properly. The package name is "Arithmetic" so
there is the Arithmetic.lean file in the base directory and then all other
files should go in the "Arithmetic" folder and be imported with
import Arithmetic.<module>. The command lake build builds the package.