Lean
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.
. The command lake build
builds the package.