feat(lean): Add support for while loops

[abentkamp]

This PR adds support for simple while loops. Panic freedom of the loop in the test gets verified fully automatically.

Future work:

• support while loops with returns and continues
• implement a better default tactic to prove invariant and termination measure being pure
• add an attribute to allow the user to replace this default tactic

[maximebuyse]

Looks good. I am curious to see how we can deal with more complicated situations, as there are many different things to prove (panic freedom of invariant, condition, body, termination metric, etc., propagation of the invariant), I imagine we'll have to make the default tactic powerful enough as it might be impractical to allow custom tactics for all these different proofs.