add LEAN example file

[haraldschilly]

in particular, a first-steps document, where such an example file explains what the UI in cocalc shows and that it works with files ending in ".lean", etc.

below, a very simple example should be enough.