Even if the environment is Cygwin, the compiler might still be the one
from MinGW, so the script no longer relies on uname.

- rounding to nearest, ties to zero
- optimal error for FLT rounding: error_le_opt_FLT
- a few lemmas about rounding to nearest

It is now needed only by the correctness theorems.

This commit also introduces a type class for (prec < emax).

Same as IEEE754.Binary but type full_float becomes
SpecFloat.spec_float and binary_float loses the NaN sign and payload.

By conditional compilation, this is a Module Import of
Coq.Floats.SpecFloat with Coq >= 8.11 or a copy SpecFloatCopy
otherwise.

Add Zceil_lb

See merge request !13

Zfloor had Zfloor_ub, just make things more homogenous.