Tests: add proof for test_coherent_mul
A proof for the function test_coherent_mul
in https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/pbt/test_tez_repr.ml
Unfortunately, the tests are more precise than the properties we verified in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/tez_repr/ . Thus, a good part of the proof is done by hand rather than calling existing lemma. Also, here I use nia
instead of lia
as this works better for some cases, typically with multiplications and division operators.
Edited by Guillaume Claret