docs: init first sketch

[RaitoBezarius]

This is a first sketch of user documentation for Aeneas to prove things with Lean.

This adds a factorial example with Alectryon and scaffolding from the Lean original project.