* Fix an issue in a proof of the hashmap

* Improve scalar_decr_tac

* Improve the error message of scalar_tac and add the missing Termination.lean

* Make progress on the proofs of the hashmap

* Make a minor modification to the hashmap

* Make progress on the hashmap

* Make progress on the proofs

* Make progress on the proofs

* Make progress on the proof of the hashmap

* Progress on the proofs of the hashmap

* Update a proof

* Update the Charon pin

* Make minor modifications to the hashmap

* Regenerate the tests

* Regenerate the hashmap

* Add lemmas to the Lean backend

* Make progress on the proofs of the hashmap

* Make a minor fix

* Finish the proof about the hashmap

* Update scalar_tac

* Make a minor modification in the hashmap

* Update the proofs of the hashmap

---------

Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local>
Co-authored-by: Son Ho <sonho@Sons-MBP.lan>

`HasIntPred` enable generation of facts based on specific terms in the
context rather than their types, e.g. if the "length of a list" occurs
in the context, generate the fact 0 ≤ length of that list, which can be
further used for `scalar_tac` automation to discharge bounds goals.

The aim is to use it to simplify various height related computations,
e.g. whenever "height of a (left ; right) tree" is encountered, generate
"height left < height of a (left ; right) tree", etc.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>