Compare: add domain

In this MR we will do a lot of cleaning for the verification of comparison operations. Indeed, the current setting does not allow us to verify all the compare operators in the code, or make it very complex.

The main we do is the following: we add a domain for the validity of the compare functions, so that we can express validity on non-total compare operators.