Directed subtraction soundness for conventional IEEE formats

Subtraction reuses directed addition after exact sign-bit negation of the right operand. Generic finite-value negation semantics turn the resulting sum bounds into real subtraction bounds.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_subDown_le {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.subDown y).toEReal ≤ ↑(x.toReal - y.toReal)

Downward-rounded subtraction is a lower bound on exact real subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_subUp {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : ↑(x.toReal - y.toReal) ≤ (x.subUp y).toEReal

Exact real subtraction is bounded above by upward-rounded subtraction.