feat: improve the Lean backend

[sonmarcho]

This PR does the following:

• update massert to operate on decidable propositions rather than booleans, leading to cleaner expressions in the goals when displaying code
• add some lemmas about lists, SRRange.foldWhile, more scalar_tac_simps, natify, bvify lemmas
• add models for wrapping_mul
• fix minor issues with scalar_tac, progress and progress*
• introduces the simp_lists tactic to simplify expressions of the shape ((set l i x).set j y).get k (in practice, it works by doing conditional rewritings and discharging arithmetic proof obligations with scalar_tac )