feat: `Rat.toFloat`

[digama0]

This adds an implementation of exact (IEEE conforming) rounding from Rat to Float rounding nearest ties to even. Note that unlike most other lean functions (but like most float functions), division by zero results in Float.inf or Float.nan, not 0.