Feature request: even more float functions

I have more requests:

• Float.abs : Float → Float seems to be missing
• Float.toInt : Float → Int, where it returns a best-effort GMP integer if the float value wouldn't fit in to a scalar value.
• Float.mantissa: Float → Int and Float.exponent : Float → Int to return the mantissa and exponent parts of the float such that mantissa * 2^exponent is equal to the original float.
• NaN ≠ NaN, so equality is not reflexive for Float which seems bad for Lean even if that is the correct behaviour in float spec.

The issue lists four Float-related requests: toInt, mantissa, exponent, and NaN equality behavior; Float.abs is already marked complete. Start by checking the existing Float API and its equality semantics, then determine how each unchecked behavior is specified and tested. Done means the requested functions and equality behavior are implemented consistently with Lean's float model.