Resolve "Add correct compare definitions"

This MR got longer than I expected. The main changes are:

• having a correct definition of the compare primitive for integers: it should only return -1, 0 or +1 and not be the difference in Z of the two inputs like we did before. This was wrong both because it is not the OCaml behavior and it could exceed the bounds of int, int32 or int64;
• removing the Compare.wrap_compare usage in many places, as this function to normalize the output of comparison functions to -1, 0 or +1 is not needed anymore in many places;
• having more direct definitions for the various comparison operators (<i, >=i64, ...), using the >?, >=?, ... Coq primitives instead of going through the compare operator;
• fixing some conversion functions between the various kinds of integers, to normalize the results.

These changes broke one proof in Saturation_repr.v about the multiplication. Hopefully with these changes we should be fully correct now for our definitions of integers.

Closes #34 (closed)