stdlib: proper postcondition for (=) on bounded integers

When the first postcondition of (=) x y is different from { result <-> x = y }, Why3 cannot convert program expression x = y into a logical formula x = y, which breaks, e.g., anonymous functions using (=) on bounded integers.

Most of examples/ passes after the change, except for several files in multiprecision:

• div
• mpz_div2exp
• mpz_mul
• mpz_sub
• powm