Directed multiplication soundness for conventional IEEE formats

For finite operands, mul x y (mode := .down) and mul x y (mode := .up) round the same exact dyadic product in opposite directions. The extended-real statements hold even when outward rounding overflows.

The bounds hold for every descriptor satisfying fmt.isIEEE = true, with no restriction to named widths.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_mul_down_le {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : toEReal (x.mul y IEEERoundingMode.down) ≤ ↑(x.toReal * y.toReal)

Downward-rounded multiplication is a lower bound on the exact real product.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_mul_up {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : ↑(x.toReal * y.toReal) ≤ toEReal (x.mul y IEEERoundingMode.up)

The exact real product is bounded above by upward-rounded multiplication.