Verify the compare function for Michelson
Verify that the function dep_compare_comparable
https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/simulations/script_comparable#dep_compare_comparable is valid. There is an old proof that got commented out and that can be a start for the new one.