Add project skeleton

[collares]

The key thing to be aware of when using Lean projects is that you should open the root directory (the one containing the lean-toolchain file) in VS Code using the "Open Folder" command, instead of opening files directly. Otherwise imports won't work (they probably don't work now either, though).

If you ever want to update the Lean version used by this project in the future, just edit the lean-toolchain file and VS Code/Emacs should pick it up automatically.