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.