Add a conference tutorial

[sonmarcho]

This PR adds a tutorial for Lean which can be used for workshops/conferences.

It also introduces many improvements (for the Lean backend):

• progress now automatically splits the conjuncts in the post-conditions (no need for the .. in progress as ⟨ x .. ⟩ anymore). It also uses a smart version of assumption which applies an assumption to a goal containing meta-variables only if there is a single matching assumption in the context (this way, we avoid spurious instantiations of meta-variables, while benefiting from a good level of automation).
• it fixes issues with scalar_tac, including performance issues, problems with the preprocessing which would not simplify the context as much as expected, better handling of natural numbers, more preprocessing to handle disjunctions, etc.
• it introduces Scalar.toNat, U32.toNat, etc.
• it introduces delaborators for the scalars. For instance, before we had the notation 1#u32 which desugared to U32.ofInt 1 (by scalar_tac). Until now it was however printed as U32.ofInt 1 ... in the goals. It now gets printed to 1#u32.
• definitions for overflow_add, ! (for scalars), Vec::resize
• it fixes type checking issues by marking the extracted trait implementations as reducible
• it introduces scalar_nf and scalar_eq_nf (which use ring_nf)
• it introduces dcases, a modified version of cases which allows to perform case disjunction about decidable propositions in a simpler manner